diff --git a/proofs/dkproof.mk b/proofs/dkproof.mk
index c5aafac0295b090a1225857f661b192dc1929fa4..7734b146a17ff824c5b9280cd9870a2ffcd4b627 100644
--- a/proofs/dkproof.mk
+++ b/proofs/dkproof.mk
@@ -2,8 +2,12 @@ KJSON   ?= keep-json
 JSON2LP ?= json2lp
 DOPTH   ?= dopth
 JQ      ?= jq
+PROVEIT ?=
 
-.SUFFIXES: .log .json .lp .dep
+.SUFFIXES: .pvs .log .json .lp .dep
+
+.pvs.log:
+	${PROVEIT} --traces -l ${.IMPSRC}
 
 .log.json:
 	${KJSON} < ${.IMPSRC} > ${.TARGET}
diff --git a/proofs/examples/Makefile b/proofs/examples/Makefile
index da151f901a85a196b693f5e573812207fdd2d427..787aaa95193d5ee006128feabf69845704d67a0c 100644
--- a/proofs/examples/Makefile
+++ b/proofs/examples/Makefile
@@ -1,8 +1,3 @@
-PROVEIT ?=
-
-.SUFFIXES: .log .pvs .prf
-
-.pvs.log: 
-	${PROVEIT} --traces -l $<
-
 all: hello.log
+
+.include "../dkproof.mk"