diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-10-23 22:46:50 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-23 22:46:50 -0700 |
commit | 00e75cb0c6aedab34740b7feadb512ea3c0c7f3d (patch) | |
tree | e046bca9e8f04be0028811682f4c4b0f6dfa475b /test/regress/regress0 | |
parent | 2f11cfd563ef96402042e9a3b0086712de660ae6 (diff) |
CBQI BV: Add ULT/SLT inverse handling. (#1268)
This adds inverse handling for ULT(BV), SLT(BV) and disequalities. Rewriting of inequalities and disequalities to equalities with slack can now be disabled with an option (--cbqi-bv-inv-in-dis-eq). Function solve_bv_constraint is now merged into solve_bv_lit.
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 new file mode 100644 index 000000000..814b0d90b --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-inv-in-dis-eq +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (= (bvand x a) b))) + +(check-sat) |