diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-16 12:20:53 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-16 12:20:53 -0500 |
| commit | 547df7cd146091674562dfa4812f10bae7765934 (patch) | |
| tree | d73fad7ff1131f4b7a1fe3f5799d54d096181fec /test | |
| parent | eae5bf6a701037238b91476de9f8d26e34976779 (diff) | |
Catch more cases of nested recursion in datatypes (#5285)
Fixes #5280.
Previously we were checking for nested recursive datatypes in expandDefinitions. This does not catch cases where the only terms of a malformed nested recursive datatype are variables. The proper place to check is in preRegisterTerm. The benchmark from that issue now gives an error.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/issue5280-no-nrec.smt2 | 8 |
2 files changed, 9 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e8b85ac31..cb3c9d9f8 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -431,6 +431,7 @@ set(regress_0_tests regress0/datatypes/is_test.smt2 regress0/datatypes/issue1433.smt2 regress0/datatypes/issue2838.cvc + regress0/datatypes/issue5280-no-nrec.smt2 regress0/datatypes/jsat-2.6.smt2 regress0/datatypes/list-bool.smt2 regress0/datatypes/model-subterms-min.smt2 diff --git a/test/regress/regress0/datatypes/issue5280-no-nrec.smt2 b/test/regress/regress0/datatypes/issue5280-no-nrec.smt2 new file mode 100644 index 000000000..f80a6796a --- /dev/null +++ b/test/regress/regress0/datatypes/issue5280-no-nrec.smt2 @@ -0,0 +1,8 @@ +; EXPECT: (error "Cannot handle nested-recursive datatype ty0") +; EXIT: 1 +(set-logic ALL) +(declare-datatype ty0 ((Emp) (Container (v2 (Set ty0))))) +(declare-fun v1 () ty0) +(assert (not ((_ is Emp) v1))) +(assert (= (v2 v1) (singleton v1))) +(check-sat) |