Age | Commit message (Expand) | Author |
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 | very small fast example for the bv fail | Dejan Jovanović |
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-08 | small fuzz examples where bv fails | Dejan Jovanović |
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 | cleaning up the expample for the future | Dejan Jovanović |
2012-06-07 | Added small test case for diseq propagation | Clark Barrett |
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 | also remove now-incorrect comment from makefile | Morgan Deters |
2012-06-06 | Fixed broken test case, removed one that is a mistake | Clark Barrett |
2012-06-06 | unconstrained regressions are now run with "make check", but with --unconstra... | Morgan Deters |
2012-06-06 | Fixing numerous issues with tests and "make dist": | 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 | svn:ignore a parallel-tests driver file that automake deposits in config/ | Morgan Deters |
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ć |
2012-05-24 | Significant changes to the internals of the equality engine. Equality is not ... | Dejan Jovanović |
2012-05-22 | This commit merges in the branch arithmetic/cprop. | Tim King |