diff options
Diffstat (limited to 'test/smt/shift_or_concat_1.sat.sail')
| -rw-r--r-- | test/smt/shift_or_concat_1.sat.sail | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/test/smt/shift_or_concat_1.sat.sail b/test/smt/shift_or_concat_1.sat.sail index 88107c50..505753b2 100644 --- a/test/smt/shift_or_concat_1.sat.sail +++ b/test/smt/shift_or_concat_1.sat.sail @@ -5,10 +5,11 @@ $include <prelude.sail> register R1 : bits(32) register R2 : bits(32) -function check_sat((): unit) -> bool = { +$property +function prop((): unit) -> bool = { let x = sail_zero_extend(R1, 64); let x = sail_shiftleft(x, 31); let y = or_vec(x, sail_zero_extend(R2, 64)); let z = R1 @ R2; - not_bool(y == z) + y == z }
\ No newline at end of file |