Age | Commit message (Expand) | Author |
2012-05-18 | removing failing regression | Dejan Jovanović |
2012-05-17 | Fixed bug 338: | Liana Hadarean |
2012-05-17 | Adding failing regression for ite type computation. | Tim King |
2012-05-16 | testcase for bug 337 | Dejan Jovanović |
2012-05-15 | test cases | Dejan Jovanović |
2012-05-14 | Fixed assertion failures in array theory | Clark Barrett |
2012-05-08 | Merging in bvprop branch, with proper bit-vector propagation. | Liana Hadarean |
2012-05-07 | Fixing a bug with TheoryArith::ppAssert() and shared terms. | Tim King |
2012-05-07 | Fixes a sign bug in the DioSolver. | Tim King |
2012-04-28 | New LogicInfo functionality. | Morgan Deters |
2012-04-24 | This commit merges in the branch branches/arithmetic/congruence into trunk. H... | Tim King |
2012-04-18 | add the missing BINARY variable in some test/regress makefiles | Kshitij Bansal |
2012-04-17 | Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo... | Tim King |
2012-04-11 | merge from arrays-clark branch | Morgan Deters |
2012-04-06 | * Smt2 printer for datatypes | François Bobot |
2012-04-05 | Support to test the "dumper" mechanism in regressions (feeding dump output ba... | Morgan Deters |
2012-04-04 | * added propagation as lemmas to TheoryBV: | Liana Hadarean |
2012-04-02 | Removing large and unused regress2 benchmarks to decrease the size of checkouts. | Tim King |
2012-03-22 | some improvements to the sharing mechanism/interface | Dejan Jovanović |
2012-03-08 | Removing QUICK_CHECK, and other unused ones, from the Theory::Effort. | Dejan Jovanović |
2012-03-01 | Partial merge from kind-backend branch, including Minisat and CNF work to | Morgan Deters |
2012-02-29 | fixing bug310 | Dejan Jovanović |
2012-02-21 | Fix for bug303. The problem was with function applications that get normalize... | Dejan Jovanović |
2012-02-20 | portfolio merge | Morgan Deters |
2012-02-16 | Last commit accidentally lacked r2778 and r2779 from integer2. I have manual... | Tim King |
2012-02-15 | This commit merges into trunk the branch branches/arithmetic/integers2 from r... | Tim King |
2012-02-07 | removing the 100 integer benchmarks from regress0, too many | Dejan Jovanović |
2012-01-25 | Adding regress1 test ooo.rf6.smt2. | Tim King |
2011-12-15 | Partial fix in arithmetic for propagating shared terms. This partially resolv... | Tim King |
2011-12-10 | attempt to fix bug 293: if a split on a trivial shared pair is requested from... | Dejan Jovanović |
2011-11-30 | disable bug288.smt so that "make check" goes through---pending integers merge... | Morgan Deters |
2011-11-30 | Simplified bug288.smt to reflect the problem in integers better. | Tim King |
2011-11-30 | Added a failing regression test corresponding to bug 289. | Tim King |
2011-11-30 | Adding a failing UFLIA benchmark corresponding to bug #288. | Tim King |
2011-11-16 | * Applying Andy's fix for datatypes bug #286; thanks for the quick work, Andy! | Morgan Deters |
2011-10-29 | support for proof regressions in other parts of the test tree | Morgan Deters |
2011-10-29 | Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::g... | Morgan Deters |
2011-10-28 | proof regressions | Morgan Deters |
2011-10-19 | Merging the branch branches/arithmetic/push-pop-support from r2247 to r2256 i... | Tim King |
2011-10-17 | Sharing work | Dejan Jovanović |
2011-10-04 | also add test case | Morgan Deters |
2011-10-04 | fixes to context-dependent caching substitutions | Morgan Deters |
2011-10-03 | user push/pop support in minisat and simplification; also bindings work | Morgan Deters |
2011-09-30 | more push/pop infrastructure, some SAT stuff | Morgan Deters |
2011-09-30 | fixes to incremental simplification, cnf routines, other stuff in preparation... | Morgan Deters |
2011-09-15 | additional stuff for sharing, | Dejan Jovanović |
2011-09-02 | Merge from my post-smtcomp branch. Includes: | Morgan Deters |
2011-09-02 | Partial merge of integers work; this is simple B&B and some pseudoboolean | Morgan Deters |
2011-07-12 | forgot to reflect naming change in makefile. fixed | Morgan Deters |
2011-07-12 | fix bug 272, array unsoundness, and some array cleanup | Morgan Deters |