From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri, 21 Aug 2015 07:26:30 +0000 (-0400)
Subject: better handling for conflicting options with nonlinear arith (bug 646)
X-Git-Tag: cvc5-1.0.0~6253
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ebaa44a4b93b00614b41ef38f36112883ee27626;p=cvc5.git

better handling for conflicting options with nonlinear arith (bug 646)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 192485dcc..66487e4a4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1544,14 +1544,23 @@ void SmtEngine::setDefaults() {
   if (d_logic.isTheoryEnabled(THEORY_ARITH) &&
       !d_logic.isLinear()) {
     if (options::produceModels()) {
+      if(options::produceModels.wasSetByUser()) {
+        throw OptionException("produce-model not supported with nonlinear arith");
+      }
       Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl;
       setOption("produce-models", SExpr("false"));
     }
     if (options::produceAssignments()) {
+      if(options::produceAssignments.wasSetByUser()) {
+        throw OptionException("produce-assignments not supported with nonlinear arith");
+      }
       Warning() << "SmtEngine: turning off produce-assignments because unsupported for nonlinear arith" << endl;
       setOption("produce-assignments", SExpr("false"));
     }
     if (options::checkModels()) {
+      if(options::checkModels.wasSetByUser()) {
+        throw OptionException("check-models not supported with nonlinear arith");
+      }
       Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << endl;
       setOption("check-models", SExpr("false"));
     }