From 9e5c9056d09cd54bc9ebb1c8a00b12db02d7dbc7 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 10 Feb 2019 18:07:06 -0600
Subject: [PATCH] test: add a logitest target

---
 Makefile          | 11 +++++++++++
 src/smt/Solver.ml |  2 +-
 tests/conf.toml   | 30 ++++++++++++++++++++++++++++++
 3 files changed, 42 insertions(+), 1 deletion(-)
 create mode 100644 tests/conf.toml

diff --git a/Makefile b/Makefile
index 08a91087..497d277d 100644
--- a/Makefile
+++ b/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
 
diff --git a/src/smt/Solver.ml b/src/smt/Solver.ml
index e38aaf80..509f1c16 100644
--- a/src/smt/Solver.ml
+++ b/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;
diff --git a/tests/conf.toml b/tests/conf.toml
new file mode 100644
index 00000000..3e243cc9
--- /dev/null
+++ b/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"
+
+
+