diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-06 11:33:33 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-06 11:33:33 -0500 |
commit | c59f4e5dbbbcef7d30ab1bba2210ec32be42563e (patch) | |
tree | ee8138c33f0c6a02a984564afc4753894a9ed2e1 /test | |
parent | 793321a0b4f9d02eb1ba7e416bd2d9fcb407ddf7 (diff) |
Refactor and document quantifiers variable elimination and conditional splitting (#2424)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/cond-var-elim-binary.smt2 | 16 |
2 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index b8b047e6d..7f33adac1 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -610,6 +610,7 @@ REG0_TESTS = \ regress0/quantifiers/cegqi-nl-sq.smt2 \ regress0/quantifiers/clock-10.smt2 \ regress0/quantifiers/clock-3.smt2 \ + regress0/quantifiers/cond-var-elim-binary.smt2 \ regress0/quantifiers/delta-simp.smt2 \ regress0/quantifiers/double-pattern.smt2 \ regress0/quantifiers/ex3.smt2 \ diff --git a/test/regress/regress0/quantifiers/cond-var-elim-binary.smt2 b/test/regress/regress0/quantifiers/cond-var-elim-binary.smt2 new file mode 100644 index 000000000..edf780b4e --- /dev/null +++ b/test/regress/regress0/quantifiers/cond-var-elim-binary.smt2 @@ -0,0 +1,16 @@ +(set-logic BV) +(set-info :status unsat) +(declare-fun k_42 () (_ BitVec 32)) +(declare-fun k_332 () (_ BitVec 32)) +(declare-fun k_28 () (_ BitVec 32)) + +(assert (and +(bvult k_332 k_42) + +(forall ((x (_ BitVec 32)) (y (_ BitVec 32))) (or + (and (not (bvult y (_ bv65539 32))) (not (= (_ bv1 32) x))) + (not (bvult k_332 (bvmul x k_42)))) ) +) +) + +(check-sat) |