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