test/smt/minmax_2.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, b) == min_int(a, b));
  true
}