Age | Commit message (Expand) | Author |
2012-06-11 | OK, now the rewrite issues are fixed | Clark Barrett |
2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
2012-06-11 | Fix for array bug with decision heuristic | Clark Barrett |
2012-06-11 | fix issue referred to in bug 352 regarding infinite loop between Substitution... | Morgan Deters |
2012-06-11 | Fixed bug 352 | Clark Barrett |
2012-06-10 | Fixed one more bug in rewriter | Clark Barrett |
2012-06-10 | Added a very fruitful assertion to the rewriter: checks that rewriting after ... | Clark Barrett |
2012-06-10 | adding an assertion to trigger the problem of bug349 and the testcase | Dejan Jovanović |
2012-06-10 | fixes for bug347 | Dejan Jovanović |
2012-06-09 | Turning on unconstrained simp for QF_AUFBV | Clark Barrett |
2012-06-09 | Cleanup and comments for the dag-ifier. Also some unit testing for it. | Morgan Deters |
2012-06-09 | Dagification of output expressions. | Morgan Deters |
2012-06-08 | The option --arith-presolve-lemmas had previously been renamed --unate-lemmas. | Morgan Deters |
2012-06-08 | Extend Printer infrastructure also to the "Result" class, meaning that differ... | Morgan Deters |
2012-06-08 | minor fixes, for Mac OS | Morgan Deters |
2012-06-08 | Fix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferring it earlier). | Morgan Deters |
2012-06-08 | handle BitVectorSignExtend in pickler | Kshitij Bansal |
2012-06-08 | threadlocal | Kshitij Bansal |
2012-06-08 | Merge from decision branch (till r3663) | Kshitij Bansal |
2012-06-07 | fixing the wrong results. arrays equality adaptor had a missing case when pro... | Dejan Jovanović |
2012-06-07 | LogicInfo locking implemented, and some initialization-order issues in SmtEng... | Morgan Deters |
2012-06-07 | Fixed performance issue with ite_simplifier on some QF_AUFBV benchmarks | Clark Barrett |
2012-06-07 | Adding EchoCommand and associated printer and parser rules: | Morgan Deters |
2012-06-07 | fixing some bugs in propagation of disequalities | Dejan Jovanović |
2012-06-06 | Don't ever call nonclausalSimplify if simplificationMode = NONE (even if | Clark Barrett |
2012-06-06 | Fixed assertion failures | Clark Barrett |
2012-06-06 | removing std::cout from trunk | Morgan Deters |
2012-06-06 | disabling a super-expensive assertions to speed up debug runs | Dejan Jovanović |
2012-06-06 | Changes to the combination mechanism, lots of details. Not done yet, there ar... | Dejan Jovanović |
2012-06-06 | Fixed problem causing crash at destruction time | Clark Barrett |
2012-06-05 | More clean-up | Clark Barrett |
2012-06-05 | Fixed a performance issue with unconstrained simplifier | Clark Barrett |
2012-06-05 | Adding missing files... | Clark Barrett |
2012-06-04 | Added preprocessing pass that propagates unconstrained values - solves all of | Clark Barrett |
2012-06-01 | add a global user-context push/pop in smt engine, just like clark's addition ... | Morgan Deters |
2012-05-31 | Fixed bug in bv: one more case where non-shared equality was getting propagated | Clark Barrett |
2012-05-31 | pass JAVA_CPPFLAGS properly | Morgan Deters |
2012-05-30 | Added BitwiseEq bitvector rewrite | Clark Barrett |
2012-05-30 | Fixed problem with array queue growing too large | Clark Barrett |
2012-05-30 | remove unused/broken check build target | Morgan Deters |
2012-05-29 | removing now-unused TheoryEngine::setLogic() interface function | Morgan Deters |
2012-05-29 | Enabled SolveEq bv rewrite | Clark Barrett |
2012-05-28 | Added some BV rewrites, fixed bugs in array theory, made ite simp work with BV | Clark Barrett |
2012-05-27 | some reordering to keep invariants | Dejan Jovanović |
2012-05-27 | Committing the work on equality engine, I need to see how it does on the regr... | Dejan Jovanović |
2012-05-27 | Another expensive function call in a Debug trace | Clark Barrett |
2012-05-27 | Another expensive function call in a Debug line | Clark Barrett |
2012-05-25 | init bug fix | Kshitij Bansal |
2012-05-25 | Checking in fix for bug 340 - somehow didn't get checked in earlier | Clark Barrett |
2012-05-24 | Separating the subtheory implementations in the bitvector theory. | Dejan Jovanović |