13 files changed, 254 insertions, 1 deletions
diff --git a/test/smt/arith.unsat.sail b/test/smt/arith.unsat.sail
new file mode 100644
index 00000000..20892ce6
--- /dev/null
+++ b/test/smt/arith.unsat.sail
@@ -0,0 +1,33 @@
+default Order dec
+
+$include <prelude.sail>
+
+$option -smt_ignore_overflow
+
+$property
+function prop(x: int, y: int, z: int) -> bool = {
+  let lo = -100000000000;
+  let hi = 100000000000;
+  if lo >= x | x >= hi | lo >= y | y >= hi | lo >= z | z >= hi then {
+    return(true)
+  };
+
+  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_C128FL.unsat.sail b/test/smt/arith_C128FL.unsat.sail
new file mode 100644
index 00000000..3a323452
--- /dev/null
+++ b/test/smt/arith_C128FL.unsat.sail
@@ -0,0 +1,34 @@
+default Order dec
+
+$include <prelude.sail>
+
+$option -smt_ignore_overflow
+
+$property
+function prop forall 'n, 0 <= 'n <= 128. (x: int(128), y: int('n), z: int) -> bool = {
+  let lo = -100000000000;
+  let hi = 100000000000;
+  if lo >= x | x >= hi | lo >= y | y >= hi | lo >= z | z >= hi then {
+    return(true)
+  };
+
+  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_assoc
+  /* 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_C64C32CB.unsat.sail b/test/smt/arith_C64C32CB.unsat.sail
new file mode 100644
index 00000000..49e0ac59
--- /dev/null
+++ b/test/smt/arith_C64C32CB.unsat.sail
@@ -0,0 +1,25 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: int(64), y: int(32), z: int(1823473425924535349753247394723984324344634534)) -> 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_FFL_1.unsat.sail b/test/smt/arith_FFL_1.unsat.sail
new file mode 100644
index 00000000..d6ba31e3
--- /dev/null
+++ b/test/smt/arith_FFL_1.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n 'm, 0 <= 'n <= 128 & 0 <= 'm <= 64. (x: int('m), y: int('n), 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
+}
+\ No newline at end of file
diff --git a/test/smt/arith_FFL_2.unsat.sail b/test/smt/arith_FFL_2.unsat.sail
new file mode 100644
index 00000000..1b095e99
--- /dev/null
+++ b/test/smt/arith_FFL_2.unsat.sail
@@ -0,0 +1,21 @@
+default Order dec
+
+$include <prelude.sail>
+
+$option -smt_ignore_overflow
+$option -smt_int_size 256
+
+$property
+function prop forall 'n 'm, 0 <= 'n <= 128 & 0 <= 'm <= 64. (x: int('m), y: int('n), z: int) -> bool = {
+  let lo = -1000;
+  let hi = 1000;
+  if lo >= z | z >= hi then {
+    return(true)
+  };
+
+  let mul_comm = x * y == y * x;
+  let mul_assoc = (x * y) * z == x * (y * z);
+  let mul_zero = x * 0 == 0;
+
+  mul_comm & mul_assoc /* & mul_zero */
+}
diff --git a/test/smt/arith_FFL_3.unsat.sail b/test/smt/arith_FFL_3.unsat.sail
new file mode 100644
index 00000000..87dbc498
--- /dev/null
+++ b/test/smt/arith_FFL_3.unsat.sail
@@ -0,0 +1,19 @@
+default Order dec
+
+$include <prelude.sail>
+
+$option -smt_ignore_overflow
+$option -smt_int_size 256
+
+$property
+function prop forall 'n 'm, 0 <= 'n <= 128 & 0 <= 'm <= 64. (x: int('m), y: int('n), z: int) -> bool = {
+  let lo = -100000000000;
+  let hi = 100000000000;
+  if lo >= z | z >= hi then {
+    return(true)
+  };
+
+  let add_mul_distrib = x * (y + z) == (x * y) + (x * z);
+
+  add_mul_distrib
+}
+\ No newline at end of file
diff --git a/test/smt/arith_FFL_4.unsat.sail b/test/smt/arith_FFL_4.unsat.sail
new file mode 100644
index 00000000..29902af6
--- /dev/null
+++ b/test/smt/arith_FFL_4.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n 'm, 0 <= 'n <= 128 & 0 <= 'm <= 64. (x: int('m), y: int('n), z: int) -> 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
+}
+\ No newline at end of file
diff --git a/test/smt/arith_LC32L.unsat.sail b/test/smt/arith_LC32L.unsat.sail
new file mode 100644
index 00000000..547a5cb1
--- /dev/null
+++ b/test/smt/arith_LC32L.unsat.sail
@@ -0,0 +1,27 @@
+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_LCBL.unsat.sail b/test/smt/arith_LCBL.unsat.sail
new file mode 100644
index 00000000..879217fc
--- /dev/null
+++ b/test/smt/arith_LCBL.unsat.sail
@@ -0,0 +1,33 @@
+default Order dec
+
+$include <prelude.sail>
+
+$option -smt_ignore_overflow
+
+$property
+function prop(x: int, y: int(248534734259245353247394723984172394), z: int) -> bool = {
+  let lo = -100000000000;
+  let hi = 100000000000;
+  if lo >= x | x >= hi | lo >= z | z >= hi then {
+    return(true)
+  };
+
+  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_LFL.unsat.sail b/test/smt/arith_LFL.unsat.sail
new file mode 100644
index 00000000..3fdcd0fd
--- /dev/null
+++ b/test/smt/arith_LFL.unsat.sail
@@ -0,0 +1,33 @@
+default Order dec
+
+$include <prelude.sail>
+
+$option -smt_ignore_overflow
+
+$property
+function prop forall 'n, 0 <= 'n <= 128. (x: int, y: int('n), z: int) -> bool = {
+  let lo = -100000000000;
+  let hi = 100000000000;
+  if lo >= x | x >= hi | lo >= y | y >= hi | lo >= z | z >= hi then {
+    return(true)
+  };
+
+  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/run_tests.py b/test/smt/run_tests.py
index fb5a0ebd..c9cadec3 100755
--- a/test/smt/run_tests.py
+++ b/test/smt/run_tests.py
@@ -23,7 +23,7 @@ def test_smt(name, solver, sail_opts):
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 step('sail {} -smt {} -o {}'.format(sail_opts, filename, basename))
-                step('{} {}_prop.smt2 1> {}.out'.format(solver, basename, basename))
+                step('timeout 20s {} {}_prop.smt2 1> {}.out'.format(solver, basename, basename))
                 if re.match('.+\.sat\.sail$', filename):
                     step('grep -q ^sat$ {}.out'.format(basename))
                 else:
diff --git a/test/smt/rv_add_0.sat.sail b/test/smt/rv_add_0.sat.sail
index d0e8a5f5..4f1a28c5 100644
--- a/test/smt/rv_add_0.sat.sail
+++ b/test/smt/rv_add_0.sat.sail
@@ -2,6 +2,8 @@ default Order dec
 
 $include <prelude.sail>
 
+$option -smt_ignore_overflow
+
 type xlen       : Int  = 32
 type xlen_bytes : Int  = 4
 type xlenbits   : Type = bits(xlen)
diff --git a/test/smt/rv_add_0.unsat.sail b/test/smt/rv_add_0.unsat.sail
index cddc5c7a..ed45112e 100644
--- a/test/smt/rv_add_0.unsat.sail
+++ b/test/smt/rv_add_0.unsat.sail
@@ -2,6 +2,8 @@ default Order dec
 
 $include <prelude.sail>
 
+$option -smt_ignore_overflow
+
 type xlen       : Int  = 32
 type xlen_bytes : Int  = 4
 type xlenbits   : Type = bits(xlen)