| 2012-09-26 |
Morgan Deters | bug #398 test (bug was resolved last night), and a... |
blob | commitdiff | raw |
| 2012-09-21 |
Morgan Deters | SMT-LIBv2 compliance updates: |
blob | commitdiff | raw | diff to current |
| 2012-09-16 |
Morgan Deters | enable bug regression for bug 382 |
blob | commitdiff | raw | diff to current |
| 2012-09-15 |
Morgan Deters | bug testcase for model generation |
blob | commitdiff | raw | diff to current |
| 2012-09-06 |
Morgan Deters | Remove SmtEngine::getStackLevel(), which exposed implem... |
blob | commitdiff | raw | diff to current |
| 2012-08-28 |
Morgan Deters | fix regression tests for automake 1.11 and automake... |
blob | commitdiff | raw | diff to current |
| 2012-08-21 |
Morgan Deters | add some incremental in-tree regressions |
blob | commitdiff | raw | diff to current |
| 2012-07-27 |
François Bobot | Merge quantifiers2-trunk: |
blob | commitdiff | raw | diff to current |
| 2012-07-08 |
Morgan Deters | Bugs resolved by this commit: #314, #322, #359, #364... |
blob | commitdiff | raw | diff to current |
| 2012-06-22 |
François Bobot | TPTP: add parser for cnf and fof |
blob | commitdiff | raw | diff to current |
| 2012-06-14 |
Morgan Deters | don't run rewriterules regressions by default; fixes... |
blob | commitdiff | raw | diff to current |
| 2012-06-13 |
Dejan Jovanović | removing bug233 until morgan commits the actual file |
blob | commitdiff | raw | diff to current |
| 2012-06-13 |
Morgan Deters | adding some regressions to the usual regressions runs... |
blob | commitdiff | raw | diff to current |
| 2012-06-13 |
Kshitij Bansal | decision regressions, all but one fail |
blob | commitdiff | raw | diff to current |
| 2012-06-11 |
Morgan Deters | Merge from quantifiers2-trunkmerge branch. |
blob | commitdiff | raw | diff to current |
| 2012-06-06 |
Morgan Deters | unconstrained regressions are now run with "make check... |
blob | commitdiff | raw | diff to current |
| 2012-06-06 |
Morgan Deters | Fixing numerous issues with tests and "make dist": |
blob | commitdiff | raw | diff to current |
| 2012-05-18 |
Tim King | This commit adds TypeNode::leastCommonTypeNode(). ... |
blob | commitdiff | raw | diff to current |
| 2012-05-18 |
Dejan Jovanović | removing failing regression |
blob | commitdiff | raw | diff to current |
| 2012-05-17 |
Tim King | Adding failing regression for ite type computation. |
blob | commitdiff | raw | diff to current |
| 2012-05-15 |
Dejan Jovanović | test cases |
blob | commitdiff | raw | diff to current |
| 2012-04-11 |
Morgan Deters | merge from arrays-clark branch |
blob | commitdiff | raw | diff to current |
| 2012-04-05 |
Morgan Deters | Support to test the "dumper" mechanism in regressions... |
blob | commitdiff | raw | diff to current |
| 2012-03-22 |
Dejan Jovanović | some improvements to the sharing mechanism/interface |
blob | commitdiff | raw | diff to current |
| 2012-03-01 |
Morgan Deters | Partial merge from kind-backend branch, including Minis... |
blob | commitdiff | raw | diff to current |
| 2012-02-29 |
Dejan Jovanović | fixing bug310 |
blob | commitdiff | raw | diff to current |
| 2012-02-21 |
Dejan Jovanović | Fix for bug303. The problem was with function applicati... |
blob | commitdiff | raw | diff to current |
| 2012-02-20 |
Morgan Deters | portfolio merge |
blob | commitdiff | raw | diff to current |
| 2012-02-15 |
Tim King | This commit merges into trunk the branch branches/arith... |
blob | commitdiff | raw | diff to current |
| 2011-11-30 |
Morgan Deters | disable bug288.smt so that "make check" goes through... |
blob | commitdiff | raw | diff to current |
| 2011-11-30 |
Tim King | Adding a failing UFLIA benchmark corresponding to bug... |
blob | commitdiff | raw | diff to current |
| 2011-10-29 |
Morgan Deters | Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF... |
blob | commitdiff | raw | diff to current |
| 2011-10-28 |
Morgan Deters | proof regressions |
blob | commitdiff | raw | diff to current |
| 2011-09-30 |
Morgan Deters | fixes to incremental simplification, cnf routines,... |
blob | commitdiff | raw | diff to current |
| 2011-07-05 |
Dejan Jovanović | updated preprocessing and rewriting input equalities... |
blob | commitdiff | raw | diff to current |
| 2011-05-23 |
Morgan Deters | Merge from arrays2 branch. |
blob | commitdiff | raw | diff to current |
| 2011-05-05 |
Morgan Deters | Merge from nonclausal-simplification-v2 branch: |
blob | commitdiff | raw | diff to current |
| 2011-04-23 |
Morgan Deters | fix for parser/tests for ANTLR 3.2 (it was working... |
blob | commitdiff | raw | diff to current |
| 2011-04-23 |
Morgan Deters | * reviewed BooleanSimplification, added documentation... |
blob | commitdiff | raw | diff to current |
| 2011-04-18 |
Morgan Deters | Partial merge from datatypes-merge branch: |
blob | commitdiff | raw | diff to current |
| 2011-03-30 |
Morgan Deters | improve recent low-coverage complaints |
blob | commitdiff | raw | diff to current |
| 2011-03-30 |
Morgan Deters | Add Valuation::getSatValue() so that theories can acces... |
blob | commitdiff | raw | diff to current |
| 2011-03-26 |
Morgan Deters | fix typo |
blob | commitdiff | raw | diff to current |
| 2011-03-25 |
Morgan Deters | This is a merge from the "theoryfixes+cdattrhash" branc... |
blob | commitdiff | raw | diff to current |
| 2011-03-10 |
Morgan Deters | ITE removal in TheoryEngine was not properly handling... |
blob | commitdiff | raw | diff to current |
| 2011-03-05 |
Morgan Deters | adding three features to CVC parser that drastically... |
blob | commitdiff | raw | diff to current |
| 2011-01-05 |
Dejan Jovanović | Commit for the theory engine and rewriter changes.... |
blob | commitdiff | raw | diff to current |
| 2010-12-14 |
Morgan Deters | fix to static learning application in UF, resolves... |
blob | commitdiff | raw | diff to current |
| 2010-11-16 |
Morgan Deters | SmtEngine now fails with a ModalException if --incremen... |
blob | commitdiff | raw | diff to current |
| 2010-11-15 |
Morgan Deters | fix some things with the build system (make dist, make... |
blob | commitdiff | raw | diff to current |
| 2010-11-09 |
Dejan Jovanović | Lemmas on demand work, push-pop, some cleanup. |
blob | commitdiff | raw | diff to current |
| 2010-10-20 |
Morgan Deters | fix bug #220 (assertion fails if no query/check-sat... |
blob | commitdiff | raw | diff to current |
| 2010-10-07 |
Morgan Deters | SMT-LIBv2 (define-fun...) command now functional; does... |
blob | commitdiff | raw | diff to current |
| 2010-09-20 |
Dejan Jovanović | hooking up the bitvector tests |
blob | commitdiff | raw | diff to current |
| 2010-09-14 |
Tim King | * added test/regress/regress0/arith for easy arithmetic... |
blob | commitdiff | raw | diff to current |
| 2010-08-17 |
Morgan Deters | Merge from "cc" branch: |
blob | commitdiff | raw | diff to current |
| 2010-07-22 |
Tim King | Added test file for fuzzsmt bug, bug187.smt2. |
blob | commitdiff | raw | diff to current |
| 2010-07-07 |
Christopher L. Conway | Disabling failing tests |
blob | commitdiff | raw | diff to current |
| 2010-07-07 |
Christopher L. Conway | Adding tests for precedence of arithmetic in CVC inputs |
blob | commitdiff | raw | diff to current |
| 2010-07-06 |
Morgan Deters | add regressions from bug reports |
blob | commitdiff | raw | diff to current |
| 2010-07-04 |
Morgan Deters | make dist && make distcheck functional, other fixes |
blob | commitdiff | raw | diff to current |
| 2010-06-17 |
Morgan Deters | fix some minor annoyances in the regression test Makefi... |
blob | commitdiff | raw | diff to current |
| 2010-06-04 |
Christopher L. Conway | Enabling RDL/IDL in SMT v1 and adding some simple tests |
blob | commitdiff | raw | diff to current |
| 2010-06-03 |
Tim King | Fixes 2 issues with assignments. The first is construct... |
blob | commitdiff | raw | diff to current |
| 2010-05-27 |
Tim King | Preregistration has been turned on. Highly experimental... |
blob | commitdiff | raw | diff to current |
| 2010-05-27 |
Christopher L. Conway | Adding NodeManager::prepareToBeDestroyed() (Fixes:... |
blob | commitdiff | raw | diff to current |
| 2010-05-27 |
Morgan Deters | fix bug 120; competition mode regression failures for... |
blob | commitdiff | raw | diff to current |
| 2010-05-19 |
Tim King | Significant revision to theory/arith. The new draft... |
blob | commitdiff | raw | diff to current |
| 2010-05-14 |
Christopher L. Conway | Adding ITE tests |
blob | commitdiff | raw | diff to current |
| 2010-05-14 |
Christopher L. Conway | Adding rudimentary ITE handling in CnfStream |
blob | commitdiff | raw | diff to current |
| 2010-05-03 |
Morgan Deters | main driver supports .smt2 input, added an smt2 regress... |
blob | commitdiff | raw | diff to current |
| 2010-04-04 |
Morgan Deters | * Node::isAtomic() now looks at an "atomic" attribute... |
blob | commitdiff | raw | diff to current |
| 2010-03-30 |
Christopher L. Conway | Merging from branches/antlr3 (r246:354) |
blob | commitdiff | raw | diff to current |
| 2010-03-10 |
Christopher L. Conway | Adding preliminary let/flet support to SMT parser ... |
blob | commitdiff | raw | diff to current |
| 2010-03-09 |
Dejan Jovanović | (no commit message) |
blob | commitdiff | raw | diff to current |
| 2010-03-08 |
Dejan Jovanović | adding simple-uf to the regressions, and the code that... |
blob | commitdiff | raw | diff to current |
| 2010-02-22 |
Morgan Deters | resolve bug 32; public-facing interface functions in... |
blob | commitdiff | raw | diff to current |
| 2010-02-11 |
Christopher L. Conway | Adding precedence regressions |
blob | commitdiff | raw | diff to current |
| 2010-02-09 |
Dejan Jovanović | Changes to the CNF conversion and the SAT solver. All... |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Morgan Deters | build system for multi-level regressions |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Morgan Deters | test infrastructure updated for multiple-level regressions |
blob | commitdiff | raw | diff to current |
|
projects / cvc5.git / history