diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-01 15:29:05 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-01 15:29:05 -0500 |
| commit | a8c785aaadae1f5316e8e12455b362c468db4106 (patch) | |
| tree | b20875279c6d698acb7af76121244d07d47ba342 /test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 | |
| parent | b0fd7761fc36fc53141cb1486e9cb19dd00ae5f3 (diff) | |
Apply preprocessing to counterexample lemmas in CEGQI (#2027)
Diffstat (limited to 'test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2')
| -rw-r--r-- | test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 b/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 new file mode 100644 index 000000000..6cbe4db5c --- /dev/null +++ b/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 @@ -0,0 +1,22 @@ +(set-info :smt-lib-version 2.6) +(set-logic BV) +(set-info :status sat) +(declare-fun x () (_ BitVec 32)) +(assert +(forall ((u (_ BitVec 32)) (w (_ BitVec 32)) (z (_ BitVec 32)) (m (_ BitVec 32)) (n (_ BitVec 32))) (or + (not (= + (bvadd (bvmul (_ bv2 32) w) (bvmul (_ bv2 32) n)) + (bvadd (bvneg (bvadd (bvmul (_ bv2 32) u) (bvmul (_ bv2 32) z) (bvmul (_ bv2 32) m) x)) (_ bv1 32)) + )) +)) +) +(assert (not +(and + (forall ((m (_ BitVec 32)) (n (_ BitVec 32))) + (not (= + (bvadd (bvneg (bvadd m x)) (_ bv1 32)) + (bvmul (_ bv2 32) n) + )) +)))) +(check-sat) +(exit) |