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/regress/regress0/quantifiers | |
| parent | 32530dad5747665df4086abd2c4fabff15bb7d12 (diff) | |
Make quantifiers strategies exit immediately when in conflict (#2099)
Diffstat (limited to 'test/regress/regress0/quantifiers')
| -rw-r--r-- | test/regress/regress0/quantifiers/issue2035.smt2 | 16 |
1 files changed, 16 insertions, 0 deletions
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) |