projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c254649) | patch
Fix related to parametric sorts whose interpretation is finite due to uninterpreted...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 23 May 2016 19:28:29 +0000 (14:28 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 23 May 2016 19:28:29 +0000 (14:28 -0500)
commitb13d2f7921a65b8921ef37b38a2d4579f7c911a2
treedf7e49fb4318fe58631ca4c4305125dd4fc32afetree
parentc254649c8dadd9f0d94f09bf46b21f93b2c67c07commit | diff
Fix related to parametric sorts whose interpretation is finite due to uninterpreted sorts + FMF.  Generalizes previous fix in term registration visitor.
12 files changed:
src/expr/datatype.cpp diff | blob | history
src/expr/datatype.h diff | blob | history
src/expr/type_node.cpp diff | blob | history
src/expr/type_node.h diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/type_enumerator.cpp diff | blob | history
src/theory/datatypes/type_enumerator.h diff | blob | history
src/theory/quantifiers/quant_split.cpp diff | blob | history
src/theory/term_registration_visitor.cpp diff | blob | history
src/theory/theory_model.cpp diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/sc-crash-052316.smt2 [new file with mode: 0644] blob