projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ea1a0bc) | patch
Minor fixes to model construction to take singleton equivalence classes into account...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 12 Aug 2016 17:09:45 +0000 (12:09 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 12 Aug 2016 17:09:59 +0000 (12:09 -0500)
commit7c2ea3c85221fce27d8c4d2b7d41a00e103b8cf5
tree534cb48ad237e5ac6e682f55ea7104c9bb1b97f7tree
parentea1a0bc57bbd90421c76c2c4811882ce3ef90eb3commit | diff
Minor fixes to model construction to take singleton equivalence classes into account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/quantifiers/ceg_instantiator.cpp diff | blob | history
src/theory/theory_model.cpp diff | blob | history
test/regress/regress0/sets/Makefile.am diff | blob | history
test/regress/regress0/sets/dt-simp-mem.smt2 [new file with mode: 0644] blob