Age | Commit message (Expand) | Author |
2012-08-05 | Disable failing datatypes regression, pending solution to bug #370. | Morgan Deters |
2012-08-04 | isConst() rule for datatypes | Morgan Deters |
2012-08-03 | Comparisons for LogicInfos, and associated tests | Morgan Deters |
2012-08-03 | ArrayStoreAll infrastructure | Morgan Deters |
2012-08-01 | fixes to some *clean targets | Morgan Deters |
2012-07-31 | Options merge. This commit: | Morgan Deters |
2012-07-27 | Minor cleanup after today's commits: | Morgan Deters |
2012-07-27 | removing unecessary files | Andrew Reynolds |
2012-07-27 | merging fmf-devel branch, includes refactored datatype theory, updates to mod... | Andrew Reynolds |
2012-07-27 | Merge quantifiers2-trunk: | François Bobot |
2012-07-26 | Datatype enumerator work. This version is not a "fair" enumerator, but I got... | Morgan Deters |
2012-07-18 | a few fixes for java system test | Morgan Deters |
2012-07-16 | now passes "make distcheck", which does important checks for the release (e.g... | Morgan Deters |
2012-07-16 | fix compiler warning in unit test | Morgan Deters |
2012-07-16 | stronger two_smt_engines test | Morgan Deters |
2012-07-16 | fix inadvertent change to system test | Morgan Deters |
2012-07-16 | Support for having two SmtEngines with the same ExprManager. | Morgan Deters |
2012-07-14 | Type enumerator infrastructure and uninterpreted constant support. No suppor... | Morgan Deters |
2012-07-14 | fix a warning in unit test compilation | Morgan Deters |
2012-07-08 | Bugs resolved by this commit: #314, #322, #359, #364, #365. | Morgan Deters |
2012-07-07 | Various fixes to documentation---typos, some incomplete documentation fixed, ... | Morgan Deters |
2012-06-28 | Fixed bug in bv rewriter that caused wrong answer in SMT-COMPsmtcomp2012-resubmission-2 | Clark Barrett |
2012-06-22 | TPTP: add parser for cnf and fof | François Bobot |
2012-06-17 | enabling theoryof=term for quantifiers with sharing | Dejan Jovanović |
2012-06-17 | fixing wrong assertion | Dejan Jovanović |
2012-06-17 | fixing makefile error that brakes build | Dejan Jovanović |
2012-06-17 | Fix array bug causing incorrect answers | Clark Barrett |
2012-06-16 | Adding the failing QF_AUFLIA regression mentioned in last commit. | Kshitij Bansal |
2012-06-16 | changing theoryOf in shared mode with arrays to move equalities to arrays | Dejan Jovanović |
2012-06-15 | Fixes some assertion failures | Clark Barrett |
2012-06-15 | one bug fixed | Kshitij Bansal |
2012-06-14 | fixing the problems with the bvminisat. there was a case when things would ge... | Dejan Jovanović |
2012-06-14 | add failing regression, move error up | Kshitij Bansal |
2012-06-14 | bug fixes in justification heuristic | Kshitij Bansal |
2012-06-14 | enabling fixed bug345 case | Dejan Jovanović |
2012-06-14 | fixes for the hasTerm issues in the shared database under the decision heuristic | Dejan Jovanović |
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 | This commit: | Kshitij Bansal |
2012-06-14 | failing quantifier | Kshitij Bansal |
2012-06-14 | add passing regression | Kshitij Bansal |
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 a loop to internally assert constraints that are marked as true. | Tim King |
2012-06-13 | add passing regression | Kshitij Bansal |
2012-06-13 | enabling regressions from last night, all fixed | Dejan Jovanović |