From: Morgan Deters <mdeters@gmail.com>
Date: Sun, 30 Sep 2012 23:20:49 +0000 (+0000)
Subject: minor changes to arithmetic assertions involving nonlinearity and models (related... 
X-Git-Tag: cvc5-1.0.0~7757
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f95c6698e5d57b7142b76f29e977168b5bb5ac8c;p=cvc5.git

minor changes to arithmetic assertions involving nonlinearity and models (related to bug 405)
---

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 2b0d9149d..17c2b51f3 100644
--- 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;