projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 61acf8c) | patch
This commit:
authorKshitij Bansal <kshitij@cs.nyu.edu>
Thu, 14 Jun 2012 16:46:44 +0000 (16:46 +0000)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Thu, 14 Jun 2012 16:46:44 +0000 (16:46 +0000)
commit8da791368c6d8cad97ff81b2b540c90ffdebc7ff
tree2b628eb20576338f6bb0dd8a425c7fcbd37b7a87tree
parent61acf8c8d621799984e622b65598caec4acceb52commit | diff
This commit:
* enables decision heuristic (justification) for QF_BV and QF_AUFBV
* disables a failing regression in aufbv (because of equality engine
  assert failure trigerred by above change)
* moves around the init procedure smt_engine
* destruction time issues because of moving this -- still to be fixed,
  currently get around by not destucting stuff in driver
src/decision/decision_engine.cpp diff | blob | history
src/decision/decision_engine.h diff | blob | history
src/main/driver.cpp diff | blob | history
src/prop/prop_engine.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
test/regress/regress0/aufbv/Makefile.am diff | blob | history