projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 591649f) | patch
Bug fix instantiations for fmf-bound-int. Disable nested pre-skolemization for non...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 9 Jun 2015 09:45:14 +0000 (11:45 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 9 Jun 2015 09:45:14 +0000 (11:45 +0200)
commit3fbe87912dbffe70cf01fdf0b4652960998ea480
tree252c48277f8d2946823d80610c2065148fc8422etree
parent591649f4631e348b65b61d3f1f4ccfe1f6baf7cccommit | diff
Bug fix instantiations for fmf-bound-int.  Disable nested pre-skolemization for non-UF logics.  Update SMT COMP scripts accordingly.
contrib/run-script-smtcomp2015 diff | blob | history
contrib/run-script-smtcomp2015-assertions diff | blob | history
contrib/run-script-smtcomp2015-experimental diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/rep_set.cpp diff | blob | history