SMT: Add a fuzzing tool for the SMT builtins

5 files changed, 49 insertions, 16 deletions

diff --git a/test/smt/arith_LC32L.unsat.sail b/test/smt/arith_LC32L.unsat.sail
index 547a5cb1..82184bf8 100644
--- a/test/smt/arith_LC32L.unsat.sail
+++ b/test/smt/arith_LC32L.unsat.sail
@@ -2,26 +2,11 @@ default Order dec
 
 $include <prelude.sail>
 
-$option -smt_ignore_overflow
-
 $property
 function prop(x: int, y: int(32), z: int) -> bool = {
   let add_comm  = x + y == y + x;
   let add_assoc = (x + y) + z == x + (y + z);
   let add_id  = x + 0 == x;
 
-  let mul_comm = x * y == y * x;
-  let mul_assoc = (x * y) * z == x * (y * z);
-  let mul_zero = x * 0 == 0;
-
-  let add_mul_distrib = x * (y + z) == (x * y) + (x * z);
-
-  let add_neg_zero = x + negate(x) == 0;
-  let add_neg_sub  = x + negate(y) == x - y;
-  let neg_neg = negate(negate(x)) == x;
-
   add_comm & add_assoc & add_id
-  & mul_comm & mul_assoc & mul_zero
-  & add_mul_distrib
-  & add_neg_zero & add_neg_sub & neg_neg
-}
\ No newline at end of file
+}
diff --git a/test/smt/arith_LC32L_1.unsat.sail b/test/smt/arith_LC32L_1.unsat.sail
new file mode 100644
index 00000000..82184bf8
--- /dev/null
+++ b/test/smt/arith_LC32L_1.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: int, y: int(32), z: int) -> bool = {
+  let add_comm  = x + y == y + x;
+  let add_assoc = (x + y) + z == x + (y + z);
+  let add_id  = x + 0 == x;
+
+  add_comm & add_assoc & add_id
+}
diff --git a/test/smt/arith_LC32L_2.unsat.sail b/test/smt/arith_LC32L_2.unsat.sail
new file mode 100644
index 00000000..9a29fe13
--- /dev/null
+++ b/test/smt/arith_LC32L_2.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: int, y: int(32), z: int) -> bool = {
+  let mul_comm = x * y == y * x;
+  let mul_zero1 = x * 0 == 0;
+  let mul_zero2 = y * 0 == 0;
+
+  mul_comm & mul_zero1 & mul_zero2
+}
\ No newline at end of file
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
+}
diff --git a/test/smt/arith_LC32L_4.unsat.sail b/test/smt/arith_LC32L_4.unsat.sail
new file mode 100644
index 00000000..e94ab2c3
--- /dev/null
+++ b/test/smt/arith_LC32L_4.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: int, y: int(32)) -> bool = {
+  let add_neg_zero = x + negate(x) == 0;
+  let add_neg_sub  = x + negate(y) == x - y;
+  let neg_neg = negate(negate(x)) == x;
+
+  add_neg_zero & add_neg_sub & neg_neg
+}