From 0e52056981fe17884c748df3af25f510d265a6e9 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 14 Apr 2021 16:34:22 -0700 Subject: [PATCH] Pull in fix for #872 and add a test case. --- deps/saw-core | 2 +- intTests/test0068_zerobv/test.saw | 7 +++++++ intTests/test0068_zerobv/test.sh | 3 +++ 3 files changed, 11 insertions(+), 1 deletion(-) create mode 100644 intTests/test0068_zerobv/test.saw create mode 100755 intTests/test0068_zerobv/test.sh diff --git a/deps/saw-core b/deps/saw-core index 6e32c659fd..e4c59543fc 160000 --- a/deps/saw-core +++ b/deps/saw-core @@ -1 +1 @@ -Subproject commit 6e32c659fdadfcf99d3d586e7dcda2b7bd9a0e10 +Subproject commit e4c59543fc7520d6cfa3d44b0602a3274685b35d diff --git a/intTests/test0068_zerobv/test.saw b/intTests/test0068_zerobv/test.saw new file mode 100644 index 0000000000..17bbe02871 --- /dev/null +++ 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 new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test0068_zerobv/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw