projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 94fe6a0) | patch
Ensure model construction for parametric sorts involving uninterpreted sorts respect...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 14 Jan 2016 23:18:49 +0000 (00:18 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 14 Jan 2016 23:18:49 +0000 (00:18 +0100)
commit081351e87edeb52facba0d0abc2e933433480444
tree8d0192c895c4103877e12673c0927d25e53a3db3tree
parent94fe6a0d525bff3cdd4450b2abd04eb2cb044308commit | diff
Ensure model construction for parametric sorts involving uninterpreted sorts respect cardinality bounds on when finite model finding is enabled.
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model.h diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/dt-proper-model.smt2 [new file with mode: 0755] blob