test/smt/arith_LC32L_3.unsat.sail


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

default Order dec

$include <prelude.sail>

$option -smt_ignore_overflow

$property
function prop(x: int, y: int(32), z: int) -> bool = {
  if  -10000 <= x & x <= 10000 & -10000 <= z & z <= 10000 then
    (x * y) * z == x * (y * z)
  else true
}