test/smt/minmax_1.sat.sail


1
2
3
4
5
6
7
8
9
10
11
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
}