diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-08 22:08:52 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-08 20:08:52 -0800 |
| commit | e0846857d7f0a926203695315b565b3541175525 (patch) | |
| tree | ee11d9f081808f194929f3700603b729dd2e1d5c /test/regress | |
| parent | 6444abbbcf5f298045c32ce3d69033b8f93a41d8 (diff) | |
Ensure CEGQI is applied for parametric datatypes when applicable (#5628)
Previously was a bug computing the argument types of parametric datatypes.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/cegqi-par-dt-simple.smt2 | 7 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 590c2fef2..0bb5c9ef7 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -765,6 +765,7 @@ set(regress_0_tests regress0/quantifiers/cbqi-lia-dt-simp.smt2 regress0/quantifiers/cegqi-nl-simp.cvc regress0/quantifiers/cegqi-nl-sq.smt2 + regress0/quantifiers/cegqi-par-dt-simple.smt2 regress0/quantifiers/clock-10.smt2 regress0/quantifiers/clock-3.smt2 regress0/quantifiers/cond-var-elim-binary.smt2 diff --git a/test/regress/regress0/quantifiers/cegqi-par-dt-simple.smt2 b/test/regress/regress0/quantifiers/cegqi-par-dt-simple.smt2 new file mode 100644 index 000000000..1b72d3ba8 --- /dev/null +++ b/test/regress/regress0/quantifiers/cegqi-par-dt-simple.smt2 @@ -0,0 +1,7 @@ +; EXPECT: unsat +(set-logic ALL) +(declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T)))))) + +(declare-const x (List Int)) +(assert (not (exists ((y (List Int))) (= x (tail y))))) +(check-sat) |