diff options
| author | makaimann <makaim@stanford.edu> | 2018-05-21 14:07:48 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-21 14:07:48 -0700 |
| commit | d5e51b2f33773837768a5d89f9be2928f1551d27 (patch) | |
| tree | cea2c17665183e1de534d8238726a28d008fba21 /test | |
| parent | caf65a13994dc1d39cc31a8cea76c6a7fddb338c (diff) | |
Handle IMPLIES in bool-to-bv and test it in regress0 (#1929)
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) |