Remove too strict assertion to allow for approximate models (#5168)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 30 Sep 2020 17:41:36 +0000 (19:41 +0200)
committerGitHub <noreply@github.com>
Wed, 30 Sep 2020 17:41:36 +0000 (12:41 -0500)
commit2bd861b27f6e340ea5f6739ac57bb6ffa61ffbfc
tree0b5fae9aa5a4a3b70f6828955cc2cc8330d3b6d3
parent5ac936654df0f214e308a48116dcf6190d6255e2
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
src/theory/arith/theory_arith.cpp