From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 30 Sep 2020 17:41:36 +0000 (+0200)
Subject: Remove too strict assertion to allow for approximate models (#5168)
X-Git-Tag: cvc5-1.0.0~2780
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2bd861b27f6e340ea5f6739ac57bb6ffa61ffbfc;p=cvc5.git

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 755822d2a..25643200f 100644
--- 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 f16e0a297..d84f666be 100644
--- 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;