Age | Commit message (Expand) | Author |
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 | Detect multiply-defined :named annotations and issue an error. | Morgan Deters |
2013-05-20 | Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive m... | Morgan Deters |
2013-05-20 | Compliance fixes for :named annotations: they must name closed subterms, the ... | Morgan Deters |
2013-05-20 | Don't allow get-model & co after a user push/pop | Morgan Deters |
2013-05-20 | As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => t... | Morgan Deters |
2013-05-20 | Fix for equality-chaining of Booleans in SMT-LIBv2. | Morgan Deters |
2013-05-20 | Fix destruction issue in GetValueCommand leading to crash. | Morgan Deters |
2013-05-20 | Better error on invalid logic strings. | Morgan Deters |
2013-05-20 | Better error on illegal (pop N); also more compliant SMT-LIB error messages i... | Morgan Deters |
2013-05-20 | A couple of fixes to the get-option command for compliance with SMT-LIB. | Morgan Deters |
2013-05-20 | Disallow construction of (_ BitVec 0). | Morgan Deters |
2013-05-20 | Fixed "success" response to (push N) / (pop N) with N > 1. | Morgan Deters |
2013-05-20 | Fix to empty response to (get-assignment). | Morgan Deters |
2013-05-20 | configure fix for building with glpk on redhat, perhaps others | Morgan Deters |
2013-05-20 | minor changes to language bindings | Morgan Deters |
2013-05-20 | disable Logic-checking with finite model finding for now, since FMF uses Rati... | Morgan Deters |
2013-05-20 | Fix erroneous results when the logic was incorrectly specified (by throwing L... | Morgan Deters |
2013-05-17 | Add support for --dump-models option, in preparation for casc. | Andrew Reynolds |
2013-05-17 | As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => t... | Morgan Deters |
2013-05-17 | Fix for equality-chaining of Booleans in SMT-LIBv2. | Morgan Deters |
2013-05-17 | Fix destruction issue in GetValueCommand leading to crash. | Morgan Deters |
2013-05-17 | Better error on invalid logic strings. | Morgan Deters |
2013-05-17 | Better error on illegal (pop N); also more compliant SMT-LIB error messages i... | Morgan Deters |
2013-05-17 | A couple of fixes to the get-option command for compliance with SMT-LIB. | Morgan Deters |
2013-05-17 | Disallow construction of (_ BitVec 0). | Morgan Deters |
2013-05-17 | Fixed "success" response to (push N) / (pop N) with N > 1. | Morgan Deters |
2013-05-17 | Fix to empty response to (get-assignment). | Morgan Deters |
2013-05-16 | configure fix for building with glpk on redhat, perhaps others | Morgan Deters |
2013-05-16 | Fix minor bug in full_model_check.cpp | Andrew Reynolds |
2013-05-16 | minor changes to language bindings | Morgan Deters |
2013-05-14 | added some extra options to the bit-vector theory | lianah |
2013-05-14 | Add support for quantifier patterns in smt2 printer. | Andrew Reynolds |
2013-05-14 | Refactoring to separate old and new model building/checking code. | Andrew Reynolds |
2013-05-11 | Preliminary version of finite model finding over bounded integer quantificati... | Andrew Reynolds |
2013-05-10 | disable Logic-checking with finite model finding for now, since FMF uses Rati... | Morgan Deters |
2013-05-10 | now proofs print mapping between atom and propositional variable as a comment... | lianah |
2013-05-10 | Update casc run script. Work on compliance for SZS output. | Andrew Reynolds |
2013-05-10 | fixes to the proof system so it works with theory lemmas and explanations | lianah |
2013-05-10 | Fix erroneous results when the logic was incorrectly specified (by throwing L... | Morgan Deters |
2013-05-10 | Add documentation for --disable-fmf-inst-gen, which removes a warning | Morgan Deters |
2013-05-09 | Add simplification option --fo-prop-quant. Add model support for new model-c... | Andrew Reynolds |
2013-05-09 | Merge branch 'master' of ssh://github.com/CVC4/CVC4 | Kshitij Bansal |
2013-05-09 | Changing the integer normal form to increase matching. | Tim King |
2013-05-08 | Add new method for checking candidate models, --fmf-fmc. Add infrastructure ... | Andrew Reynolds |
2013-05-08 | rm decision/relevancy | Kshitij Bansal |
2013-05-08 | Removing arithmetic compile warning for release | Morgan Deters |
2013-05-08 | final updates for smt-eval script | Morgan Deters |
2013-05-08 | Fixed assertion bug | Clark Barrett |