From 55ef1bf844fcaaddc2a3dd299a48670fea017d97 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 6 Dec 2019 14:23:21 -0600 Subject: [PATCH] Throw exception instead of warning for approximate models (#3542) --- src/smt/smt_engine.cpp | 8 ++++---- 1 file 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 -- 2.30.2