1 files changed, 12 insertions, 0 deletions
diff --git a/test/smt/minmax_1.sat.sail b/test/smt/minmax_1.sat.sail
new file mode 100644
index 00000000..09119db0
--- /dev/null
+++ b/test/smt/minmax_1.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, a) == max_int(b, a));
+  true
+}