diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-02 22:13:12 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-02 22:13:12 +0000 |
commit | b8a010d260c90efa5433a71dd317a03f051c2592 (patch) | |
tree | 40f716a0895d2302954b79de45893368af942723 /src/theory | |
parent | 6e283659af0f95505e92a1826953509537f9d216 (diff) |
* re-enable some Z3 extended commands:
declare-const
declare-funs
declare-preds
define
simplify
* don't output --help on bad options, just invite user to try --help
* Datatypes from SMT2 parser now name the tester is-cons (e.g.)
* unknown results produce models, --check-model doesn't fail hard for
incorrect unknown models. removed the assert that kept arithmetic
from producing models if it saw nonlinear
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 17c2b51f3..f8f0756c7 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -2075,7 +2075,7 @@ DeltaRational TheoryArith::getDeltaValueWithNonlinear(TNode n, bool& failed) { void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){ AlwaysAssert(d_qflraStatus == Result::SAT); - AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints"); + //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints"); Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl; |