diff --git a/Makefile b/Makefile
index 5b073ab0..18d559cb 100644
--- a/Makefile
+++ b/Makefile
@@ -35,6 +35,9 @@ snapshots:
 $(TESTTOOL)-quick: snapshots
 	$(TESTTOOL) run $(TESTOPTS) \
 	  --csv snapshots/quick-$(DATE).csv --task sidekick-smt-quick
+$(TESTTOOL)-quick-proofs: snapshots
+	$(TESTTOOL) run $(TESTOPTS) \
+	  --csv snapshots/quick-$(DATE).csv --task sidekick-smt-quick-proofs --proof-dir out-proofs-$(DATE)/
 $(TESTTOOL)-local: snapshots
 	$(TESTTOOL) run $(TESTOPTS) \
 	  --csv snapshots/quick-$(DATE).csv --task sidekick-smt-local
diff --git a/tests/benchpress.sexp b/tests/benchpress.sexp
index 48521f35..f3c57fdd 100644
--- a/tests/benchpress.sexp
+++ b/tests/benchpress.sexp
@@ -7,6 +7,20 @@
   (unknown "Timeout|Unknown")
   (version "git:."))
 
+(proof_checker
+  (name quip)
+  (cmd "quip -nc $proof_file --problem=$file")
+  (valid "^OK$")
+  (invalid "^FAIL$"))
+
+(prover
+  (name sidekick-dev-p)
+  (inherits sidekick-dev)
+  (cmd "$cur_dir/../sidekick --no-check --time $timeout $file -o $proof_file")
+  (proof_ext ".quip.gz")
+  (proof_checker quip)
+  (produces_proof true))
+
 (dir
   (path $cur_dir)
   (pattern ".*.(smt2|cnf)$")
@@ -20,6 +34,16 @@
       (timeout 10)
       (dirs ($cur_dir/sat $cur_dir/unsat $cur_dir/pigeon)))))
 
+; only unsat SMT problems
+(task
+  (name sidekick-smt-quick-proofs)
+  (action
+    (run_provers
+      (provers (sidekick-dev sidekick-dev-p z3))
+      (timeout 10)
+      (pattern ".*.smt2$")
+      (dirs ($cur_dir/unsat)))))
+
 (task
   (name sidekick-smt-local)
   (action