diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/bv/bool-to-bv.smt2 | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/bool-to-bv.smt2 b/test/regress/regress0/bv/bool-to-bv.smt2 index 9d336af96..92c7e4117 100644 --- a/test/regress/regress0/bv/bool-to-bv.smt2 +++ b/test/regress/regress0/bv/bool-to-bv.smt2 @@ -4,6 +4,9 @@ (declare-fun x2 () (_ BitVec 3)) (declare-fun x1 () (_ BitVec 3)) (declare-fun x0 () (_ BitVec 3)) +(declare-fun b1 () Bool) +(declare-fun b2 () Bool) (assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1))) (assert (= #b000 x2)) +(assert (=> b1 b2)) (check-sat) |