1 files changed, 12 insertions, 0 deletions
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
+}