Age | Commit message (Expand) | Author |
2013-07-24 | Regressions now checking models on unknown too. But quantifiers don't have t... | Morgan Deters |
2013-07-24 | Don't allow --stats if not a statistics-enabled build | Morgan Deters |
2013-07-23 | (get-info :all-options) to get option values; also command-line option sugges... | Morgan Deters |
2013-07-17 | Fix bug 516; include some bug testcases. | Morgan Deters |
2013-07-11 | Support for TPTP's TFF0 (with arithmetic) | Morgan Deters |
2013-07-11 | Fix for Boolean-term rewriting and LAMBDAs | Morgan Deters |
2013-07-06 | Model output is now const; this related to bug 519 | Morgan Deters |
2013-06-25 | Merge branch '1.2.x' | Morgan Deters |
2013-06-24 | Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al... | Morgan Deters |
2013-06-21 | Fix failure in non-assertion builds on incorrect SmtEngine use. | Morgan Deters |
2013-06-08 | Fixes for Boolean terms in arrays (including fix for bug 517). | Morgan Deters |
2013-06-07 | One more case for arrays of Boolean. | Morgan Deters |
2013-06-07 | Fix for bug 517. | Morgan Deters |
2013-05-20 | Merge branch '1.2.x' | Morgan Deters |
2013-05-20 | Fix error reporting on use of (nonlinear) div,mod,/ symbols | Morgan Deters |
2013-05-20 | Don't allow get-model & co after a user push/pop | Morgan Deters |
2013-05-20 | Fix for equality-chaining of Booleans in SMT-LIBv2. | Morgan Deters |
2013-05-20 | Better error on invalid logic strings. | Morgan Deters |
2013-05-20 | Fix to empty response to (get-assignment). | Morgan Deters |
2013-05-17 | Add support for --dump-models option, in preparation for casc. | Andrew Reynolds |
2013-05-17 | Fix for equality-chaining of Booleans in SMT-LIBv2. | Morgan Deters |
2013-05-17 | Better error on invalid logic strings. | Morgan Deters |
2013-05-17 | Fix to empty response to (get-assignment). | Morgan Deters |
2013-05-09 | Add simplification option --fo-prop-quant. Add model support for new model-c... | Andrew Reynolds |
2013-05-08 | Add new method for checking candidate models, --fmf-fmc. Add infrastructure ... | Andrew Reynolds |
2013-05-08 | final updates for smt-eval script | Morgan Deters |
2013-05-06 | Disables justification stop only for LRA if the problem contains no ites. Thi... | Tim King |
2013-05-02 | Merge branch 'master' of https://github.com/CVC4/CVC4 | lianah |
2013-05-01 | Fix to dumping re: boolean terms, datatypes | Morgan Deters |
2013-05-01 | Fix to boolean-terms; resolves bug #507 | Morgan Deters |
2013-05-01 | added back BitwiseEq rule | lianah |
2013-04-30 | innd examples are solved fast, but destruction assertion fail | lianah |
2013-04-30 | uncompiling new bv to bool lifting | lianah |
2013-04-30 | finished implementing bv to bool lifting and added --bv-to-bool option | lianah |
2013-04-23 | Theory "alternates" support | Morgan Deters |
2013-04-18 | making sure sat context is zero when user context is popped to 0 in SmtEngine... | lianah |
2013-04-18 | fixing destruction order in SmtEngine | lianah |
2013-04-03 | * changing the bitblast-eager to bitblast on pre-register | Dejan Jovanović |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
2013-04-01 | update copyrights | Morgan Deters |
2013-04-01 | Fix regression error by turning off model-based solver when models are on | Clark Barrett |
2013-04-01 | Turning on model based array solver for QF_AX | Clark Barrett |
2013-04-01 | Made eager lemmas an option, enabled for QF_AX | Clark Barrett |
2013-04-01 | Disabling eager array index splitting for QF_AX | Clark Barrett |
2013-04-01 | Fixes for two bugs: | Morgan Deters |
2013-04-01 | Merging some cleanup work: | Morgan Deters |
2013-04-01 | Fix bug 491 and related issues with checkModel() and quantifiers. Enabling p... | Morgan Deters |
2013-03-30 | Disabling eager array index splitting for QF_AUFLIA | Clark Barrett |
2013-03-29 | make Boolean term conversion partially non-recursive (resolves bug 501) | Morgan Deters |
2013-03-26 | Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac | Morgan Deters |