diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-22 20:47:27 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-22 20:47:27 -0500 |
| commit | 83d07f5d7662557f2087136563606872b217511a (patch) | |
| tree | 1b59be1925f5c0831e0e0ce4eaa293e060ccc40f /test/regress/regress1/quantifiers/qe-partial.smt2 | |
| parent | 9c02423e90cf9cb8509d4ca6565acba06e6f9b2d (diff) | |
More regressions that increase coverage (#2354)
Diffstat (limited to 'test/regress/regress1/quantifiers/qe-partial.smt2')
| -rw-r--r-- | test/regress/regress1/quantifiers/qe-partial.smt2 | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/qe-partial.smt2 b/test/regress/regress1/quantifiers/qe-partial.smt2 new file mode 100644 index 000000000..6f414fb2c --- /dev/null +++ b/test/regress/regress1/quantifiers/qe-partial.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: +; SCRUBBER: sed -e 's/(not (>= (+ .* (\* (- 1) .*)) 1))$/(not (>= (+ TERMA (\* (- 1) TERMB)) 1))/' +; EXPECT: (not (>= (+ TERMA (* (- 1) TERMB)) 1)) +(set-logic LIA) +(set-info :status unsat) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(get-qe-disjunct (exists ((x Int)) (and (<= a x) (or (<= x b) (<= x c))))) |