test: add a logitest target

Makefile

@@ -32,6 +32,17 @@ clean:
 test:
 	@dune runtest
 
+TESTOPTS ?= -j $(J)
+TESTTOOL=logitest
+DATE=$(shell date +%FT%H:%M)
+
+logitest-quick:
+	@mkdir -p snapshots
+	$(TESTTOOL) run -c tests/conf.toml tests/ $(TESTOPTS) \
+	  --meta `git rev-parse HEAD` --summary snapshots/quick-$(DATE).txt \
+	  --csv snapshots/quick-$(DATE).csv
+
+
 install: build-install
 	@dune install
 

src/smt/Solver.ml

@@ -225,7 +225,7 @@ let solve ?(on_exit=[]) ?(check=true) ~assumptions (self:t) : res =
   let r = Sat_solver.solve ~assumptions (solver self) in
   match r with
   | Sat_solver.Sat st ->
-    Log.debugf 0 (fun k->k "SAT");
+    Log.debugf 1 (fun k->k "SAT");
     let lits f = st.iter_trail f (fun _ -> ()) in
     let m = Theory_combine.mk_model (th_combine self) lits in
     do_on_exit ~on_exit;

tests/conf.toml

@@ -0,0 +1,30 @@
+
+provers = [ "sidekick", "read-status" ]
+default_expect = "sat"
+
+[sidekick]
+
+binary = "./sidekick"
+cmd = "./sidekick -no-check -time $timeout $file"
+unsat = "Unsat"
+sat = "Sat"
+unknown = "Timeout|Unknown"
+version = "git:."
+
+[read-status]
+
+cmd = "grep :status $file"
+unsat = ":status unsat"
+sat = ":status sat"
+
+[test]
+
+timeout=10
+problems = ".*\\.(smt2|cnf)"
+provers = [ "sidekick", ]
+dir = [ "." ]
+
+expect = "program:read-status"
+
+
+