diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-04 14:34:21 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-04 14:34:21 -0500 |
commit | d367c9f9b299a15fb970d62df04d3df22b7ca08d (patch) | |
tree | 6629e5c12cc8629398e81bcf15608f5493536b6b /test | |
parent | 32530dad5747665df4086abd2c4fabff15bb7d12 (diff) |
Make quantifiers strategies exit immediately when in conflict (#2099)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/issue2035.smt2 | 16 |
2 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 63593c662..ca9b88ecf 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -621,6 +621,7 @@ REG0_TESTS = \ regress0/quantifiers/issue1805.smt2 \ regress0/quantifiers/issue2031-bv-var-elim.smt2 \ regress0/quantifiers/issue2033-macro-arith.smt2 \ + regress0/quantifiers/issue2035.smt2 \ regress0/quantifiers/lra-triv-gn.smt2 \ regress0/quantifiers/macros-int-real.smt2 \ regress0/quantifiers/macros-real-arg.smt2 \ diff --git a/test/regress/regress0/quantifiers/issue2035.smt2 b/test/regress/regress0/quantifiers/issue2035.smt2 new file mode 100644 index 000000000..4c677d352 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue2035.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --inst-when=full --full-saturate-quant +; EXPECT: unsat +(set-logic AUFLIA) +(set-info :status unsat) +(declare-fun _substvar_37_ () Int) +(declare-fun _substvar_33_ () Int) +(declare-fun _substvar_32_ () Int) +(declare-sort A 0) +(declare-sort PZA 0) +(declare-fun MS (Int A PZA) Bool) +(declare-fun length (PZA Int) Bool) +(declare-fun p () PZA) +(assert (! (exists ((n55 Int)) (and true true (forall ((x862 Int) (x863 A) (x864 A)) (=> (and (MS x862 x863 p) (MS x862 x864 p)) (= x863 x864))) true)) :named hyp30)) +(assert (! (exists ((x1298 A) (x1299 A) (x1300 Int)) (exists ((x1302 Int)) (length p 0))) :named hyp42)) +(assert (! (not (exists ((n67 Int)) (and true true (forall ((x1308 Int) (x1309 A) (x1310 A)) (=> (and (exists ((i114 Int)) (and true true (= _substvar_32_ _substvar_33_) (exists ((x1312 Int)) (and (forall ((x1313 Int)) (=> (length p 0) (= x1312 (+ (- 0 _substvar_33_) 1)))) (MS x1312 x1309 p))))) (exists ((i115 Int)) (and true true (= _substvar_32_ _substvar_37_) (exists ((x1315 Int)) (and (forall ((x1316 Int)) (=> (length p 0) (= x1315 (+ (- 0 _substvar_37_) 1)))) (MS x1315 x1310 p)))))) (= x1309 x1310))) true))) :named goal)) +(check-sat) |