From 42d5255231a833279e58f498b156478997ec1cfe Mon Sep 17 00:00:00 2001
From: Claire Wolf <claire@symbioticeda.com>
Date: Mon, 20 Jul 2020 17:17:49 +0200
Subject: [PATCH 1/2] Add "make test"

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
---
 Makefile | 69 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 69 insertions(+)

diff --git a/Makefile b/Makefile
index 62f452a..7f0a29d 100644
--- a/Makefile
+++ b/Makefile
@@ -17,6 +17,9 @@ help:
 	@echo "make html"
 	@echo "    build documentation in docs/build/html/"
 	@echo ""
+	@echo "make test"
+	@echo "    run examples"
+	@echo ""
 	@echo "make clean"
 	@echo "    cleanup"
 	@echo ""
@@ -34,6 +37,72 @@ else
 	chmod +x $(DESTDIR)$(PREFIX)/bin/sby
 endif
 
+test: \
+  test_demo1 test_demo2 test_demo3 \
+  test_abstract_abstr test_abstract_props \
+  test_demos_fib_cover test_demos_fib_prove test_demos_fib_live \
+  test_multiclk_dpmem \
+  test_puzzles_djb2hash test_puzzles_pour853to4 test_puzzles_wolfgoatcabbage \
+  test_puzzles_primegen_primegen test_puzzles_primegen_primes_pass test_puzzles_primegen_primes_fail \
+  test_quickstart_demo test_quickstart_cover test_quickstart_prove test_quickstart_memory
+
+test_demo1:
+	python3 sbysrc/sby.py -f sbysrc/demo1.sby
+
+test_demo2:
+	python3 sbysrc/sby.py -f sbysrc/demo2.sby
+
+test_demo3:
+	python3 sbysrc/sby.py -f sbysrc/demo3.sby
+
+test_abstract_abstr:
+	cd docs/examples/abstract && python3 ../../../sbysrc/sby.py -f abstr.sby
+
+test_abstract_props:
+	cd docs/examples/abstract && python3 ../../../sbysrc/sby.py -f props.sby
+
+test_demos_fib_cover:
+	cd docs/examples/demos && python3 ../../../sbysrc/sby.py -f fib.sby cover
+
+test_demos_fib_prove:
+	cd docs/examples/demos && python3 ../../../sbysrc/sby.py -f fib.sby prove
+
+test_demos_fib_live:
+	cd docs/examples/demos && python3 ../../../sbysrc/sby.py -f fib.sby live
+
+test_multiclk_dpmem:
+	cd docs/examples/multiclk && python3 ../../../sbysrc/sby.py -f dpmem.sby
+
+test_puzzles_djb2hash:
+	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f djb2hash.sby
+
+test_puzzles_pour853to4:
+	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f pour_853_to_4.sby
+
+test_puzzles_wolfgoatcabbage:
+	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f wolf_goat_cabbage.sby
+
+test_puzzles_primegen_primegen:
+	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f primegen.sby primegen
+
+test_puzzles_primegen_primes_pass:
+	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f primegen.sby primes_pass
+
+test_puzzles_primegen_primes_fail:
+	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f primegen.sby primes_fail
+
+test_quickstart_demo:
+	cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f demo.sby
+
+test_quickstart_cover:
+	cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f cover.sby
+
+test_quickstart_prove:
+	cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f prove.sby
+
+test_quickstart_memory:
+	cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f memory.sby
+
 html:
 	make -C docs html
 

From 0d98201dc7ae78e41c410354448dcee7a811fd4f Mon Sep 17 00:00:00 2001
From: Claire Wolf <claire@symbioticeda.com>
Date: Mon, 20 Jul 2020 19:42:10 +0200
Subject: [PATCH 2/2] Add "Unexpected response" handling to smtbmc engine

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
---
 docs/examples/puzzles/primegen.sby | 2 +-
 sbysrc/sby_engine_smtbmc.py        | 6 +++++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/docs/examples/puzzles/primegen.sby b/docs/examples/puzzles/primegen.sby
index 20e5072..6d88b88 100644
--- a/docs/examples/puzzles/primegen.sby
+++ b/docs/examples/puzzles/primegen.sby
@@ -6,7 +6,7 @@ primes_pass
 [options]
 mode cover
 depth 1
-primes_fail: expect fail
+primes_fail: expect fail,error
 
 [engines]
 smtbmc --dumpsmt2 --progress --stbv z3
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 65933d0..6d2ffc4 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -37,7 +37,6 @@ def run(mode, job, engine_idx, engine):
             "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="])
 
     for o, a in opts:
-        print(o, a)
         if o == "--nomem":
             nomem_opt = True
         elif o == "--syn":
@@ -169,6 +168,11 @@ def run(mode, job, engine_idx, engine):
             task_status = "ERROR"
             return line
 
+        match = re.match(r"^## [0-9: ]+ Unexpected response from solver:", line)
+        if match:
+            task_status = "ERROR"
+            return line
+
         return line
 
     def exit_callback(retcode):