Remove too strict assertion to allow for approximate models (#5168)

This PR simply removes an assertion that would trigger whenever the arithmetic theory asserts a model that contains something else than a constant. This can be the case with witness terms.
In offline discussion we concluded that this discussion was overly strict. Note that these examples may still hit an error during model validation (Cannot run check-model on a model with approximate values.).
This PR also fixes a debug output I found during debugging.

Fixes #5113.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 755822d2a3360f34a534de420a477dc0ebaf5dfd..25643200fcf82e68955bda965e25f6bfefd6da42 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1610,7 +1610,8 @@ void SmtEngine::checkModel(bool hardFailure) {
   for(size_t k = 0; k < m->getNumCommands(); ++k) {
     const DeclareFunctionNodeCommand* c =
         dynamic_cast<const DeclareFunctionNodeCommand*>(m->getCommand(k));
-    Notice() << "SmtEngine::checkModel(): model command " << k << " : " << m->getCommand(k) << endl;
+    Notice() << "SmtEngine::checkModel(): model command " << k << " : "
+             << m->getCommand(k)->toString() << endl;
     if(c == NULL) {
       // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
       Notice() << "SmtEngine::checkModel(): skipping..." << endl;

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index f16e0a297f2004263a1191492f58eed621b0cef6..d84f666be9fcc20adcf265d41b6d49d73cf01260 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -158,7 +158,6 @@ bool TheoryArith::collectModelValues(TheoryModel* m,
   {
     // maps to constant of comparable type
     Assert(p.first.getType().isComparableTo(p.second.getType()));
-    Assert(p.second.isConst());
     if (m->assertEquality(p.first, p.second, true))
     {
       continue;