SMT: Add min and max functions

Allow conversion between int(n) and int in smt_conversion

1 files changed, 12 insertions, 0 deletions

diff --git a/test/smt/minmax_2.sat.sail b/test/smt/minmax_2.sat.sail
new file mode 100644
index 00000000..dd773058
--- /dev/null
+++ b/test/smt/minmax_2.sat.sail
@@ -0,0 +1,12 @@
+
+val operator == = "eq_int" : (int, int) -> bool
+
+val "max_int" : (int, int) -> int
+
+val "min_int" : (int, int) -> int
+
+$counterexample
+function prop(a: int, b: int) -> bool = {
+  assert(max_int(a, b) == min_int(a, b));
+  true
+}