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, 21 insertions, 0 deletions

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 */
+}