diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/qbv-simp.smt2')
| -rw-r--r-- | test/regress/regress0/quantifiers/qbv-simp.smt2 | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/test/regress/regress0/quantifiers/qbv-simp.smt2 b/test/regress/regress0/quantifiers/qbv-simp.smt2 index 1f72d44e4..ec4626f52 100644 --- a/test/regress/regress0/quantifiers/qbv-simp.smt2 +++ b/test/regress/regress0/quantifiers/qbv-simp.smt2 @@ -1,9 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --no-cbqi-full +; EXPECT: unsat (set-logic BV) (set-info :status unsat) (assert (forall - ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32))) + ((A (_ BitVec 8)) (B (_ BitVec 8)) (C (_ BitVec 8)) (D (_ BitVec 8))) (or (and (= A B) (= C D)) (and (= A C) (= B D))))) - + (check-sat) - + |