diff options
| -rw-r--r-- | src/smt/smt_engine.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7e18e5a6f..c034f6f23 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4647,12 +4647,12 @@ void SmtEngine::checkModel(bool hardFailure) { Notice() << "SmtEngine::checkModel(): generating model" << endl; TheoryModel* m = getAvailableModel("check model"); - // check-model is not guaranteed to succeed if approximate values were used + // check-model is not guaranteed to succeed if approximate values were used. + // Thus, we intentionally abort here. if (m->hasApproximations()) { - Warning() - << "WARNING: running check-model on a model with approximate values..." - << endl; + throw RecoverableModalException( + "Cannot run check-model on a model with approximate values."); } // Check individual theory assertions |