diff options
Diffstat (limited to 'test/smt/concat_prop128.unsat.sail')
| -rw-r--r-- | test/smt/concat_prop128.unsat.sail | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/test/smt/concat_prop128.unsat.sail b/test/smt/concat_prop128.unsat.sail index 3d8ea45f..4205db10 100644 --- a/test/smt/concat_prop128.unsat.sail +++ b/test/smt/concat_prop128.unsat.sail @@ -5,7 +5,8 @@ $include <prelude.sail> register R1 : bits(64) register R2 : bits(64) -function check_sat('sz: range(0, 64)) -> bool = { +$property +function prop('sz: range(0, 64)) -> bool = { let z: bits('sz) = sail_zeros(sz); let x: bits('sz + 64) = R1 @ z; let y: bits(64 + 'sz) = R2 @ z; @@ -14,5 +15,5 @@ function check_sat('sz: range(0, 64)) -> bool = { // A and B must be equal let A = x @ y; let B = or_vec(sail_shiftleft(padding @ x, length(y)), padding @ y); - not_bool(A == B) + A == B } |