Age | Commit message (Expand) | Author |
2013-06-04 | File inclusion in Smt2 parser. | Morgan Deters |
2013-06-04 | Add --no-condense-function-values option for explicit function models (useful... | Morgan Deters |
2013-06-04 | Merge branch '1.2.x' | Morgan Deters |
2013-06-04 | Fix clang static initialization order issue; fixes bug 512. | Morgan Deters |
2013-06-04 | Add partial support for MBQI with arrays when using --fmf-fmc. Fix constant ... | Andrew Reynolds |
2013-05-29 | Merge branch '1.2.x' | Morgan Deters |
2013-05-29 | Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with unkno... | Morgan Deters |
2013-05-29 | SMT-LIB printer updates (some missing cases). | Morgan Deters |
2013-05-29 | Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real di... | Morgan Deters |
2013-05-28 | Standardize SMT-LIBv2 set of logics to use LogicInfo. | Morgan Deters |
2013-05-23 | Refactoring to prepare for MBQI with integer quantification. Minor bug fixes. | Andrew Reynolds |
2013-05-22 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Andrew Reynolds |
2013-05-22 | Significant work on bounded integer quantification to handle non-trivial boun... | Andrew Reynolds |
2013-05-22 | Add regressions for finite model finding | Andrew Reynolds |
2013-05-21 | Merge branch '1.2.x' | Morgan Deters |
2013-05-21 | Fix bug 512: an assertion failure only appearing with clang on Mac OS, due to... | Morgan Deters |
2013-05-21 | Fix an error that valgrind found. | Morgan Deters |
2013-05-21 | Merge branch '1.2.x' | Morgan Deters |
2013-05-21 | Fix incremental bug in symmetry breaker. | 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 | 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 |