1 files changed, 12 insertions, 0 deletions
diff --git a/test/smt/arith_LC32L_3.unsat.sail b/test/smt/arith_LC32L_3.unsat.sail
new file mode 100644
index 00000000..7d97a76b
--- /dev/null
+++ b/test/smt/arith_LC32L_3.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$option -smt_ignore_overflow
+
+$property
+function prop(x: int, y: int(32), z: int) -> bool = {
+  if  -10000 <= x & x <= 10000 & -10000 <= z & z <= 10000 then
+    (x * y) * z == x * (y * z)
+  else true
+}