From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 6 Dec 2019 20:23:21 +0000 (-0600)
Subject: Throw exception instead of warning for approximate models (#3542)
X-Git-Tag: cvc5-1.0.0~3786
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=55ef1bf844fcaaddc2a3dd299a48670fea017d97;p=cvc5.git

Throw exception instead of warning for approximate models (#3542)
---

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