diff options
Diffstat (limited to 'test/smt/arith_FFL_2.unsat.sail')
| -rw-r--r-- | test/smt/arith_FFL_2.unsat.sail | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/test/smt/arith_FFL_2.unsat.sail b/test/smt/arith_FFL_2.unsat.sail index 1b095e99..3535f1d1 100644 --- a/test/smt/arith_FFL_2.unsat.sail +++ b/test/smt/arith_FFL_2.unsat.sail @@ -3,7 +3,7 @@ default Order dec $include <prelude.sail> $option -smt_ignore_overflow -$option -smt_int_size 256 +$option -smt_int_size 128 $property function prop forall 'n 'm, 0 <= 'n <= 128 & 0 <= 'm <= 64. (x: int('m), y: int('n), z: int) -> bool = { @@ -14,8 +14,7 @@ function prop forall 'n 'm, 0 <= 'n <= 128 & 0 <= 'm <= 64. (x: int('m), y: int( }; let mul_comm = x * y == y * x; - let mul_assoc = (x * y) * z == x * (y * z); let mul_zero = x * 0 == 0; - mul_comm & mul_assoc /* & mul_zero */ + mul_comm & mul_zero } |