Age | Commit message (Expand) | Author |
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 |
2012-06-12 | Enabling constant propagation | Clark Barrett |
2012-06-12 | fix a few compatibility bindings issues | Morgan Deters |
2012-06-12 | Adding constant propagation code - needs more testing - off by default | Clark Barrett |
2012-06-12 | fix ordering issue of --dump-to and --default-dag-thresh. now can be specifi... | Morgan Deters |
2012-06-11 | Fix to term normalization of integer equalities. Adds a regression test that ... | Tim King |
2012-06-11 | Fixing type comparision assertion in getEqualityStatus(). | Tim King |
2012-06-11 | fixing bitvector bugs | Dejan Jovanović |
2012-06-11 | mark a quantifiers global var as "static" so we can find it easier later | Morgan Deters |
2012-06-11 | OK, now the rewrite issues are fixed | Clark Barrett |