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