4 files changed, 49 insertions, 0 deletions
diff --git a/test/smt/sqrt.sat.sail b/test/smt/sqrt.sat.sail
new file mode 100644
index 00000000..1cb47944
--- /dev/null
+++ b/test/smt/sqrt.sat.sail
@@ -0,0 +1,9 @@
+default Order dec
+
+$include <prelude.sail>
+$include <real.sail>
+
+$counterexample
+function prop(x: real) -> bool = {
+  not_bool(sqrt(x) == 2.0);
+}
diff --git a/test/smt/sqrt.unsat.sail b/test/smt/sqrt.unsat.sail
new file mode 100644
index 00000000..6aba221c
--- /dev/null
+++ b/test/smt/sqrt.unsat.sail
@@ -0,0 +1,9 @@
+default Order dec
+
+$include <prelude.sail>
+$include <real.sail>
+
+$property
+function prop() -> bool = {
+  sqrt(4.0) == 2.0;
+}
diff --git a/test/smt/string.sat.sail b/test/smt/string.sat.sail
new file mode 100644
index 00000000..c9c45b66
--- /dev/null
+++ b/test/smt/string.sat.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "concat_str" : (string, string) -> string
+
+val "eq_string" : (string, string) -> bool
+
+overload operator == = {eq_string}
+
+$counterexample
+function prop(x : string) -> bool = {
+  let y = ", World!";
+  not_bool(concat_str(x, y) == "Hello, World!")
+}
+\ No newline at end of file
diff --git a/test/smt/string.unsat.sail b/test/smt/string.unsat.sail
new file mode 100644
index 00000000..b91abfad
--- /dev/null
+++ b/test/smt/string.unsat.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "concat_str" : (string, string) -> string
+
+val "eq_string" : (string, string) -> bool
+
+overload operator == = {eq_string}
+
+$property
+function prop(() : unit) -> bool = {
+  let x = "Hello, ";
+  let y = "World!";
+  concat_str(x, y) == "Hello, World!"
+}
+\ No newline at end of file