| Age | Commit message (Expand) | Author |
|---|
| 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 | don't run rewriterules regressions by default; fixes needed | Morgan Deters |
| 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 | failing quantifier | 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 | add passing regression | 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 | bug 346 resolved | Morgan Deters |
| 2012-06-14 | * removing rewriteEquality from the rewriter | Dejan Jovanović |
| 2012-06-13 | removing bug233 until morgan commits the actual file | Dejan Jovanović |
| 2012-06-13 | adding some regressions to the usual regressions runs; several recently-fixed... | Morgan Deters |
| 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 | revisions to the "make submission" target | Morgan Deters |
| 2012-06-13 | Don't use the "inlined" feature of ANTLR 3.2, which causes a buffer overflow ... | Morgan Deters |
| 2012-06-13 | add passing regression | Kshitij Bansal |
| 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 | enabling regressions from last night, all fixed | Dejan Jovanović |
| 2012-06-13 | enable some decision regressions | Kshitij Bansal |
| 2012-06-13 | Make d_result in DE context dependent | Kshitij Bansal |
| 2012-06-13 | Fixed definition of bvsmod | Clark Barrett |
| 2012-06-13 | decision regressions, all but one fail | Kshitij Bansal |
| 2012-06-13 | Fixes more problems in bv rewrites | Clark Barrett |
| 2012-06-13 | !(*child_it).isConst() assertion fail | Dejan Jovanović |
| 2012-06-13 | r2.node == response.node failure | Dejan Jovanović |
| 2012-06-13 | r2.node == response.node failure | Dejan Jovanović |
| 2012-06-13 | !current[0].isConst() failure | Dejan Jovanović |
| 2012-06-13 | Fixes lots of problems in bv rewrite rules and adds lots of assertions | Clark Barrett |
| 2012-06-13 | benchmark to show that we don't rewrite bvsmod correctly | Dejan Jovanović |
| 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 | missing problems | Dejan Jovanović |
| 2012-06-12 | wrong answer for bv | Dejan Jovanović |
| 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 |
