* 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.)

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;