Pull in fix for #872 and add a test case.

GaloisInc · Apr 14, 2021 · 0e52056 · 0e52056
1 parent 9b51cd1
commit 0e52056
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 1 deletion.
diff --git a/deps/saw-core b/deps/saw-core
diff --git a/intTests/test0068_zerobv/test.saw b/intTests/test0068_zerobv/test.saw
@@ -0,0 +1,7 @@
+// test case for github issue https://github.com/GaloisInc/saw-script/issues/872
+
+prove_print z3 {{ \(x:[0]) y z -> x * (y + z) == x*y + x*z }};
+print "z3 OK";
+
+prove_print w4 {{ \(x:[0]) y z -> x * (y + z) == x*y + x*z }};
+print "w4 OK";
diff --git a/intTests/test0068_zerobv/test.sh b/intTests/test0068_zerobv/test.sh
@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw
+10 −4		saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+21 −19		saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs