test/smt/add_overflow.sat.sail


1
2
3
4
5
6
7
8
9
10
11
12

default Order dec

$include <prelude.sail>

$option -smt_ignore_overflow

$counterexample
function prop(x: int, y: int) -> bool = {
  if x >= 0  & y >= 0 then {
    x + y >= 0
  } else true
}