Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-08-26 | bug 374 fix: assert litVal=desiredVal only for leaf nodes1.2.x | Kshitij Bansal | |
2013-08-26 | Bug 374 benchmarks | Kshitij Bansal | |
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-04 | Fix clang static initialization order issue; fixes bug 512. | Morgan Deters | |
2013-05-29 | Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with ↵ | Morgan Deters | |
unknown key. | |||
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 ↵ | Morgan Deters | |
division | |||
2013-05-28 | Standardize SMT-LIBv2 set of logics to use LogicInfo. | Morgan Deters | |
Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2. This led to inconsistencies---such as nonstandard logics like "QF_LIRA" being accepted in set-logic but not providing the "Real" sort. Now, the LogicInfo is used and queried, so nonstandard logics should work fine and declare the correct symbols. SMT-LIB v1.2, unfortunately, can't take advantage of this fully since symbols like "Array" have substantially different meanings in different logics. | |||
2013-05-21 | Fix bug 512: an assertion failure only appearing with clang on Mac OS, due ↵ | Morgan Deters | |
to improper ITE removal in quantifier instantiations. | |||
2013-05-21 | Fix an error that valgrind found. | Morgan Deters | |
2013-05-21 | Fix incremental bug in symmetry breaker. | Morgan Deters | |
Thanks to Christoph Sticksel for reporting this. | |||
2013-05-20 | Fix error reporting on use of (nonlinear) div,mod,/ symbols | Morgan Deters | |
2013-05-20 | Update THANKS to mention David Cok's contributions. | Morgan Deters | |
2013-05-20 | Detect multiply-defined :named annotations and issue an error. | Morgan Deters | |
Thanks to David Cok for pointing out this issue. Conflicts: library_versions | |||
2013-05-20 | Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive ↵ | Morgan Deters | |
mode. Thanks to David Cok for raising this issue. | |||
2013-05-20 | Compliance fixes for :named annotations: they must name closed subterms, the ↵ | Morgan Deters | |
names must be user-permitted names, etc. Thanks to David Cok for raising this issue. | |||
2013-05-20 | Don't allow get-model & co after a user push/pop | Morgan Deters | |
This makes us more strictly adhere to the spec, but it's useful anyway: previously we would support a get-model until the problem was explicitly changed with e.g. a new assertion. That meant you could check-sat, then pop, then get-model, but you'd only get the part of the model still in scope. This is strange, and would likely lead to problems, so it's now disabled. Thanks to David Cok for inquiring about this. | |||
2013-05-20 | As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => ↵ | Morgan Deters | |
takes n>2 args and is right-assoc. Thanks to David Cok for pointing out this issue. | |||
2013-05-20 | Fix for equality-chaining of Booleans in SMT-LIBv2. | Morgan Deters | |
Thanks to David Cok for reporting this. | |||
2013-05-20 | Fix destruction issue in GetValueCommand leading to crash. | Morgan Deters | |
Thanks to David Cok for reporting this. | |||
2013-05-20 | Better error on invalid logic strings. | Morgan Deters | |
Thanks to David Cok for reporting this issue. Conflicts: library_versions | |||
2013-05-20 | Better error on illegal (pop N); also more compliant SMT-LIB error messages ↵ | Morgan Deters | |
in some places Thanks to David Cok for reporting these issues. | |||
2013-05-20 | A couple of fixes to the get-option command for compliance with SMT-LIB. | Morgan Deters | |
Thanks to David Cok for reporting this issue. | |||
2013-05-20 | Disallow construction of (_ BitVec 0). | Morgan Deters | |
Thanks to David Cok for reporting this issue. | |||
2013-05-20 | Fixed "success" response to (push N) / (pop N) with N > 1. | Morgan Deters | |
Thanks to David Cok for reporting this issue. | |||
2013-05-20 | Fix to empty response to (get-assignment). | Morgan Deters | |
Thanks to David Cok for reporting this issue. | |||
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 ↵ | Morgan Deters | |
Rationals, making the check think arithmetic should be enabled (but it's not) | |||
2013-05-20 | Fix erroneous results when the logic was incorrectly specified (by throwing ↵ | Morgan Deters | |
LogicException). Also correct a case where sharing was doing some work during pure theory solving. | |||
2013-05-08 | Prerelease versioning for 1.2.x | Morgan Deters | |
2013-05-08 | Merge tag 'smteval2013' | Morgan Deters | |
2013-05-08 | Cutting release 1.2.1.2 | Morgan Deters | |
2013-05-08 | Removing arithmetic compile warning for release | Morgan Deters | |
2013-05-08 | update versioningsmteval2013 | Morgan Deters | |
2013-05-08 | final updates for smt-eval script | Morgan Deters | |
2013-05-08 | Fixed assertion bug | Clark Barrett | |
2013-05-07 | fix for smt-eval run script | Morgan Deters | |
2013-05-07 | BV strategy for SMT-EVAL | Morgan Deters | |
2013-05-07 | fix for nonterminating model-based array loop | Morgan Deters | |
2013-05-07 | added type checking rule to check for bit-vector constants of size 0 | lianah | |
2013-05-07 | one more fix for rewrites | lianah | |
2013-05-07 | fixed bv rewrite blow-up | lianah | |
2013-05-07 | fix for bug500 | Dejan Jovanović | |
2013-05-07 | Fixes a bug with arithmetic's new attempt solution infrastructure. This ↵ | Tim King | |
caused arithmetic to think it was in a conflict incorrectly. This lead to it not properly responding to new input and lead to an inconsistency bug. This could be triggered previously by running: ./builds/bin/cvc4 --stats --no-restrict-pivots --enable-miplib-trick --miplib-trick-subs=2 --fc-penalties --collect-pivot-stats --new-prop --dio-decomps --unconstrained-simp --fancy-final /home/taking/benchmarks/smtlib2/QF_LRA/miplib/opt1217--17.smt2 | |||
2013-05-07 | Improving arithmetic debugging output. | Tim King | |
2013-05-07 | Disabling an incorrect prototyping line from the simplex merges. Fixes bug 510. | Tim King | |
2013-05-06 | Change SMT-EVAL run-script to use Tim's best QF_LRA command-line parameters | Morgan Deters | |
2013-05-06 | fixed bv rewrite rule bug | Liana Hadarean | |