| Age | Commit message (Expand) | Author |
|---|
| 2012-02-15 | This commit merges into trunk the branch branches/arithmetic/integers2 from r... | Tim King |
| 2012-02-10 | attempt at a fix for the local regression failure (CLN linking issues on oneiric | Morgan Deters |
| 2012-02-07 | removing the 100 integer benchmarks from regress0, too many | Dejan Jovanović |
| 2012-02-06 | Fixing a bug in the integer unit tests when configured for GMP with assertion... | Tim King |
| 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-12-06 | LemmaStatus changes, as agreed to during 12/2 meeting. | Morgan Deters |
| 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 | Addressed many of the concerns raised in the public interface review of CVC4 ... | Morgan Deters |
| 2011-11-16 | * Applying Andy's fix for datatypes bug #286; thanks for the quick work, Andy! | Morgan Deters |
| 2011-11-15 | Bindings work (ocaml bindings are now sort of working); also minor cleanup | Morgan Deters |
| 2011-11-14 | public tests need to be linked against gmp/cln explicitly---looks like a subt... | 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-23 | Implement changes from yesterday morning's meeting (10/21/2011): | Morgan Deters |
| 2011-10-21 | some printing and parser fixes for problems recently uncovered | 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-13 | Interruption, time-out, and deterministic time-out ("resource-out") features. | Morgan Deters |
| 2011-10-07 | Some new Datatype public functionality, as per Chris Conway's suggestions on ... | Morgan Deters |
| 2011-10-05 | ensureLiteral() in CNF stream to support Andy's quantifiers work; an update t... | Morgan Deters |
| 2011-10-04 | also add test case | Morgan Deters |
| 2011-10-04 | fixes to context-dependent caching substitutions | Morgan Deters |
| 2011-10-04 | compatibility, bindings | Morgan Deters |
| 2011-10-04 | compat layer cleanup | 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-29 | Some base infrastructure for user push/pop; a few bugfixes to user push/pop a... | Morgan Deters |
| 2011-09-29 | some test fixes | Morgan Deters |
| 2011-09-21 | Java binding now working. Some interface types still need some work (e.g. it... | Morgan Deters |
| 2011-09-21 | considerable bindings interface work, some improvements to build | Morgan Deters |
| 2011-09-16 | some minor fixes to the cvc3 compatibility library and test case | 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-08-25 | Fixing the broken unit tests | Dejan Jovanović |
| 2011-08-17 | new implementation of lemmas on demand | Dejan Jovanović |
| 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 |
| 2011-07-11 | remove some array regressions from "make check" so nightly regressions run | Morgan Deters |
| 2011-07-11 | status of examples | Morgan Deters |
| 2011-07-11 | new array bugs ? | Morgan Deters |
| 2011-07-11 | mark the new minimized benchmark as unsat | Morgan Deters |
| 2011-07-11 | if running in QF_AX, equalities over terms of uninterpreted sort go to arrays... | Morgan Deters |
