projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: eae5bf6) | patch
Catch more cases of nested recursion in datatypes (#5285)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 16 Oct 2020 17:20:53 +0000 (12:20 -0500)
committerGitHub <noreply@github.com>
Fri, 16 Oct 2020 17:20:53 +0000 (12:20 -0500)
commit547df7cd146091674562dfa4812f10bae7765934
treed73fad7ff1131f4b7a1fe3f5799d54d096181fectree
parenteae5bf6a701037238b91476de9f8d26e34976779commit | 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.
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/datatypes/issue5280-no-nrec.smt2 [new file with mode: 0644] blob