projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 41c6b75) | patch
Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastructure...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 22 Jul 2013 19:29:28 +0000 (14:29 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 22 Jul 2013 19:29:38 +0000 (14:29 -0500)
commitbdb5789713c03cf16f0ce6178b2fdc66f96ddc9e
treed898e2b126b425641342626a625bb8d470985f1btree
parent41c6b7593504671873b25040d806ad1e50c37093commit | diff
Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastructure to BV collectModelInfo in preparation for bug fix.
14 files changed:
src/theory/bv/bitblaster.cpp diff | blob | history
src/theory/bv/bitblaster.h diff | blob | history
src/theory/bv/bv_subtheory.h diff | blob | history
src/theory/bv/bv_subtheory_bitblast.cpp diff | blob | history
src/theory/bv/bv_subtheory_bitblast.h diff | blob | history
src/theory/bv/bv_subtheory_core.cpp diff | blob | history
src/theory/bv/bv_subtheory_core.h diff | blob | history
src/theory/bv/bv_subtheory_inequality.cpp diff | blob | history
src/theory/bv/bv_subtheory_inequality.h diff | blob | history
src/theory/bv/theory_bv.cpp diff | blob | history
src/theory/quantifiers/full_model_check.cpp diff | blob | history
src/theory/quantifiers/full_model_check.h diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/theory_quantifiers.cpp diff | blob | history