projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9df318c) | patch
Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in lemmas being...
authorajreynol <andrew.j.reynolds@gmail.com>
Sat, 1 Nov 2014 12:01:31 +0000 (13:01 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Sat, 1 Nov 2014 12:01:31 +0000 (13:01 +0100)
commit6b652f7239aaf7ef1793eb115a6e7371a3ec54eb
treedb9aa05c0803fd62679262930c35705308966d1ftree
parent9df318ca1ab33001bd203c24ae57a8b5739b8f36commit | diff
Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in lemmas being rewritten).  Minor improvement to dt care graph.  Reenable regressions.
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history