diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-29 10:28:27 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-29 10:28:27 -0600 |
commit | ee75ebf00e1aa463656cd192e52d3aec224345c0 (patch) | |
tree | 5b34e2133c6d19f2264e4994379f5dc81209239e /src/smt/smt_engine.cpp | |
parent | 31efb570a9d5811fd88a34d4915d7d08c81d13fa (diff) |
Throw warning instead of error for non-constant values in check-model stages (#3844)
Fixes #3729 and fixes #3720.
This updates two more stages of check-model (checking whether values assigned to terms are constants and internally checking whether assertions belonging to theories) to only throw warnings when a term/assertion has a non-constant value in the model. This is to accommodate cases where check-model is infeasible.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 915dc603e..cde85a186 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4785,16 +4785,19 @@ void SmtEngine::checkModel(bool hardFailure) { } // (2) check that the value is actually a value - else if (!val.isConst()) { - Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl; - InternalError() - << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH " - "MODEL:" - << endl - << "model value for " << func << endl - << " is " << val << endl - << "and that is not a constant (.isConst() == false)." << endl - << "Run with `--check-models -v' for additional diagnostics."; + else if (!val.isConst()) + { + // This is only a warning since it could have been assigned an + // unevaluable term (e.g. an application of a transcendental function). + // This parallels the behavior (warnings for non-constant expressions) + // when checking whether assertions are satisfied below. + Warning() << "Warning : SmtEngine::checkModel(): " + << "model value for " << func << endl + << " is " << val << endl + << "and that is not a constant (.isConst() == false)." + << std::endl + << "Run with `--check-models -v' for additional diagnostics." + << std::endl; } // (3) check that it's the correct (sub)type |