minor changes to arithmetic assertions involving nonlinearity and models (related...

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 2b0d9149d064f13a614b7dc860fbc837d8924f8e..17c2b51f39ea430b016862b46315bb0237746467 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1949,8 +1949,8 @@ bool TheoryArith::getDeltaAtomValue(TNode n) {
 
 
 DeltaRational TheoryArith::getDeltaValue(TNode n) {
-  Assert(d_qflraStatus != Result::SAT_UNKNOWN);
-  Assert(!d_nlIncomplete);
+  AlwaysAssert(d_qflraStatus != Result::SAT_UNKNOWN);
+  AlwaysAssert(!d_nlIncomplete);
   Debug("arith::value") << n << std::endl;
 
   switch(n.getKind()) {
@@ -2007,8 +2007,8 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
 }
 
 DeltaRational TheoryArith::getDeltaValueWithNonlinear(TNode n, bool& failed) {
-  Assert(d_qflraStatus != Result::SAT_UNKNOWN);
-  Assert(d_nlIncomplete);
+  AlwaysAssert(d_qflraStatus != Result::SAT_UNKNOWN);
+  AlwaysAssert(d_nlIncomplete);
 
   Debug("arith::value") << n << std::endl;
 
@@ -2074,8 +2074,8 @@ DeltaRational TheoryArith::getDeltaValueWithNonlinear(TNode n, bool& failed) {
 }
 
 void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){
-  Assert(d_qflraStatus ==  Result::SAT);
-  Assert(!d_nlIncomplete);
+  AlwaysAssert(d_qflraStatus ==  Result::SAT);
+  AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints");
 
   Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl;