SMT: More builtins

Add some tests for arithmetic operations. Some tests fail in either Z3
or CVC4 currently, due to how overflow is handled.

1 files changed, 34 insertions, 0 deletions

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