From 2bd861b27f6e340ea5f6739ac57bb6ffa61ffbfc Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 30 Sep 2020 19:41:36 +0200 Subject: [PATCH] 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. --- src/smt/smt_engine.cpp | 3 ++- src/theory/arith/theory_arith.cpp | 1 - 2 files changed, 2 insertions(+), 2 deletions(-) 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(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; -- 2.30.2