summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-08-26bug 374 fix: assert litVal=desiredVal only for leaf nodes1.2.xKshitij Bansal
2013-08-26Bug 374 benchmarksKshitij Bansal
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-04Fix clang static initialization order issue; fixes bug 512.Morgan Deters
2013-05-29Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with ↵Morgan Deters
unknown key.
2013-05-29SMT-LIB printer updates (some missing cases).Morgan Deters
2013-05-29Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real ↵Morgan Deters
division
2013-05-28Standardize 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-21Fix bug 512: an assertion failure only appearing with clang on Mac OS, due ↵Morgan Deters
to improper ITE removal in quantifier instantiations.
2013-05-21Fix an error that valgrind found.Morgan Deters
2013-05-21Fix incremental bug in symmetry breaker.Morgan Deters
Thanks to Christoph Sticksel for reporting this.
2013-05-20Fix error reporting on use of (nonlinear) div,mod,/ symbolsMorgan Deters
2013-05-20Update THANKS to mention David Cok's contributions.Morgan Deters
2013-05-20Detect multiply-defined :named annotations and issue an error.Morgan Deters
Thanks to David Cok for pointing out this issue. Conflicts: library_versions
2013-05-20Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive ↵Morgan Deters
mode. Thanks to David Cok for raising this issue.
2013-05-20Compliance 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-20Don't allow get-model & co after a user push/popMorgan 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-20As 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-20Fix for equality-chaining of Booleans in SMT-LIBv2.Morgan Deters
Thanks to David Cok for reporting this.
2013-05-20Fix destruction issue in GetValueCommand leading to crash.Morgan Deters
Thanks to David Cok for reporting this.
2013-05-20Better error on invalid logic strings.Morgan Deters
Thanks to David Cok for reporting this issue. Conflicts: library_versions
2013-05-20Better 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-20A 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-20Disallow construction of (_ BitVec 0).Morgan Deters
Thanks to David Cok for reporting this issue.
2013-05-20Fixed "success" response to (push N) / (pop N) with N > 1.Morgan Deters
Thanks to David Cok for reporting this issue.
2013-05-20Fix to empty response to (get-assignment).Morgan Deters
Thanks to David Cok for reporting this issue.
2013-05-20configure fix for building with glpk on redhat, perhaps othersMorgan Deters
2013-05-20minor changes to language bindingsMorgan Deters
2013-05-20disable 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-20Fix 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-08Prerelease versioning for 1.2.xMorgan Deters
2013-05-08Merge tag 'smteval2013'Morgan Deters
2013-05-08Cutting release 1.2.1.2Morgan Deters
2013-05-08Removing arithmetic compile warning for releaseMorgan Deters
2013-05-08update versioningsmteval2013Morgan Deters
2013-05-08final updates for smt-eval scriptMorgan Deters
2013-05-08Fixed assertion bugClark Barrett
2013-05-07fix for smt-eval run scriptMorgan Deters
2013-05-07BV strategy for SMT-EVALMorgan Deters
2013-05-07fix for nonterminating model-based array loopMorgan Deters
2013-05-07added type checking rule to check for bit-vector constants of size 0lianah
2013-05-07one more fix for rewriteslianah
2013-05-07fixed bv rewrite blow-uplianah
2013-05-07fix for bug500Dejan Jovanović
2013-05-07Fixes 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-07Improving arithmetic debugging output.Tim King
2013-05-07Disabling an incorrect prototyping line from the simplex merges. Fixes bug 510.Tim King
2013-05-06Change SMT-EVAL run-script to use Tim's best QF_LRA command-line parametersMorgan Deters
2013-05-06fixed bv rewrite rule bugLiana Hadarean
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback