projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 48de3ac) | patch
Fixed bug in bv: one more case where non-shared equality was getting propagated
authorClark Barrett <barrett@cs.nyu.edu>
Thu, 31 May 2012 17:15:02 +0000 (17:15 +0000)
committerClark Barrett <barrett@cs.nyu.edu>
Thu, 31 May 2012 17:15:02 +0000 (17:15 +0000)
commite0ea9a22721a332be2a2354846ffdf5f72c6a6de
tree97f277ac1e6a203a3da3cfb5c41924bad86cc942tree
parent48de3ac52d0fb8656b6e4e768c74be4be3b2a883commit | diff
Fixed bug in bv: one more case where non-shared equality was getting propagated
Added a global push and pop around solving - fixes an assertion failure when
TNodes are still around in a CDHashMap at destruction time.
src/smt/smt_engine.cpp diff | blob | history
src/theory/bv/theory_bv.cpp diff | blob | history