4 files changed, 42 insertions, 0 deletions
diff --git a/test/smt/add_overflow.sat.sail b/test/smt/add_overflow.sat.sail
new file mode 100644
index 00000000..faf432e8
--- /dev/null
+++ b/test/smt/add_overflow.sat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$option -smt_ignore_overflow
+
+$counterexample
+function prop(x: int, y: int) -> bool = {
+  if x >= 0  & y >= 0 then {
+    x + y >= 0
+  } else true
+}
diff --git a/test/smt/add_overflow.unsat.sail b/test/smt/add_overflow.unsat.sail
new file mode 100644
index 00000000..3da55b55
--- /dev/null
+++ b/test/smt/add_overflow.unsat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: int, y: int) -> bool = {
+  if x >= 0  & y >= 0 then {
+    x + y >= 0
+  } else true
+}
diff --git a/test/smt/trivial_assert.sat.sail b/test/smt/trivial_assert.sat.sail
new file mode 100644
index 00000000..5c83f1dc
--- /dev/null
+++ b/test/smt/trivial_assert.sat.sail
@@ -0,0 +1,9 @@
+default Order dec
+
+$include <prelude.sail>
+
+$counterexample
+function prop(x: bits(5), y: bits(5)) -> bool = {
+  assert(x == y);
+  true
+}
diff --git a/test/smt/trivial_assert_2.unsat.sail b/test/smt/trivial_assert_2.unsat.sail
new file mode 100644
index 00000000..cfc1a5f3
--- /dev/null
+++ b/test/smt/trivial_assert_2.unsat.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: int, y: int) -> bool = {
+  if x != y then {
+    assert(x != y);
+    true
+  } else true
+}