projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 86c541c) | patch
Fix non-termination in datatype type enumerator (#3369)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 1 Nov 2019 22:06:33 +0000 (17:06 -0500)
committerGitHub <noreply@github.com>
Fri, 1 Nov 2019 22:06:33 +0000 (17:06 -0500)
commitc547bd591891ffd9211ed3859b0a67423a708f25
treeb6a046cdc9cc474102640067fe1d9d67a012ae25tree
parent86c541cdf83e0b98def5a479d1da966f2e959408commit | diff
Fix non-termination in datatype type enumerator (#3369)
13 files changed:
src/expr/datatype.cpp diff | blob | history
src/expr/datatype.h diff | blob | history
src/expr/type.cpp diff | blob | history
src/expr/type.h diff | blob | history
src/expr/type_node.cpp diff | blob | history
src/expr/type_node.h diff | blob | history
src/theory/datatypes/type_enumerator.cpp diff | blob | history
src/theory/datatypes/type_enumerator.h diff | blob | history
src/theory/quantifiers/fmf/full_model_check.cpp diff | blob | history
src/theory/theory_model_builder.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/datatypes/issue-variant-dt-zero.smt2 [new file with mode: 0644] blob
test/regress/regress1/quantifiers/issue3316.smt2 [new file with mode: 0644] blob