Age | Commit message (Expand) | Author |
2012-06-15 | Fix for incompleteness bug with decision engine: repeated simplification | Clark Barrett |
2012-06-15 | Fixing mac compilation issues. | Tim King |
2012-06-15 | one bug fixed | Kshitij Bansal |
2012-06-14 | WIP | Kshitij Bansal |
2012-06-14 | fixing the problems with the bvminisat. there was a case when things would ge... | Dejan Jovanović |
2012-06-14 | add failing regression, move error up | Kshitij Bansal |
2012-06-14 | Fixing a case for explanation of non-normal form equalities. | Tim King |
2012-06-14 | bug fixes in justification heuristic | Kshitij Bansal |
2012-06-14 | Fixing a bug related to explaining propagations with non-normalized witnesses. | Tim King |
2012-06-14 | fixes for the hasTerm issues in the shared database under the decision heuristic | Dejan Jovanović |
2012-06-14 | New substitutions implementation - fixes performance issue seen in nonclausal | Clark Barrett |
2012-06-14 | Fixed arithmetic consistency issue. The simplex conflict variable had to be ... | Tim King |
2012-06-14 | fix for clark's bug | Dejan Jovanović |
2012-06-14 | fix quantifier non-bug | Kshitij Bansal |
2012-06-14 | Removed an assertion, unneeded header file | Clark Barrett |
2012-06-14 | some changes to make CVC4 work nicely with trace executor for application tra... | Morgan Deters |
2012-06-14 | making --simplification=none the default for quantified logics; this a reques... | Morgan Deters |
2012-06-14 | bug ifx, mv | Kshitij Bansal |
2012-06-14 | restore destruction of stuff in driver | Kshitij Bansal |
2012-06-14 | This commit: | Kshitij Bansal |
2012-06-14 | The "no-tears-in-competition-mode" commit. Change all (non-driver, non-SAT-s... | Morgan Deters |
2012-06-14 | fix cout, fix statname, rm deadcode | Kshitij Bansal |
2012-06-14 | changing to a more natural propagation order in uf, seems to pay off | Dejan Jovanović |
2012-06-14 | some changes to the uf engine | Dejan Jovanović |
2012-06-14 | Brings the tuning branch into trunk. This includes the changes from restricte... | Tim King |
2012-06-14 | * removing rewriteEquality from the rewriter | Dejan Jovanović |
2012-06-13 | Added witnesses to Constraints. | Tim King |
2012-06-13 | - Added a loop to internally assert constraints that are marked as true. | Tim King |
2012-06-13 | Fixed whitespace warning on Makefile. | Tim King |
2012-06-13 | Adds debugging output to theory_engine.cpp. | Tim King |
2012-06-13 | Don't use the "inlined" feature of ANTLR 3.2, which causes a buffer overflow ... | Morgan Deters |
2012-06-13 | fix for bug 354 | Dejan Jovanović |
2012-06-13 | Fixed failing assertion when EqualityEngine is in conflict | Clark Barrett |
2012-06-13 | Make d_result in DE context dependent | Kshitij Bansal |
2012-06-13 | Fixed definition of bvsmod | Clark Barrett |
2012-06-13 | Fixes more problems in bv rewrites | Clark Barrett |
2012-06-13 | Fixes lots of problems in bv rewrite rules and adds lots of assertions | Clark Barrett |
2012-06-12 | Fix some compile warnings (but they never showed up on church) | Morgan Deters |
2012-06-12 | Fix to SMT-LIBv1 parser: QF_UF declares sort "U", but other *UF* logics do no... | Morgan Deters |
2012-06-12 | Moved some things around in the preprocessor. Now theory preprocessing gets | Clark Barrett |
2012-06-12 | Fixed fuzzing bug | Clark Barrett |
2012-06-12 | Fix to yesterday's change in arithmetic. | Tim King |
2012-06-12 | bufixes and the bugs | Dejan Jovanović |
2012-06-12 | conflicts from theories are removable | Dejan Jovanović |
2012-06-12 | Changed bitvector theory rewriter so that equalities always get rewritten to | Clark Barrett |
2012-06-12 | cleanup of exit mechanism when decisionEngine is on\n\n fixes some bugs we we... | Kshitij Bansal |
2012-06-12 | Fixed bug causing QF_LIA/solver_cvc4/incorrect1.smt and QF_LIA/solver_cvc4/in... | Clark Barrett |
2012-06-12 | Fixed failing assertion in arrays for bug 347 | Clark Barrett |
2012-06-12 | minor cleanup, and replace a "private:" in equality engine that had been remo... | Morgan Deters |
2012-06-12 | Fixed compile error | Clark Barrett |