projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bd6a13b) | patch
Always split on constructor types for datatypes involving uninterpreted sorts when...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 22 Dec 2015 12:44:05 +0000 (13:44 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 22 Dec 2015 12:44:05 +0000 (13:44 +0100)
commit75003d97ad485f8840310e652a74872f5950538d
tree0d7b44ff11ffdf48495ed5c165f7344671e0c3b5tree
parentbd6a13bbb46c272561c01b7783f62ff7be091c2ccommit | diff
Always split on constructor types for datatypes involving uninterpreted sorts when finite model finding is enabled, add regressions.
src/expr/datatype.cpp diff | blob | history
src/expr/datatype.h diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/quantifiers/first_order_model.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/forall_unit_data.smt2 diff | blob | history
test/regress/regress0/fmf/forall_unit_data2.smt2 [new file with mode: 0755] blob
test/regress/regress0/fmf/sc_bad_model_1221.smt2 [new file with mode: 0755] blob