From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 20 Jun 2014 19:13:23 +0000 (-0400)
Subject: Fatal error if --unconstrained-simp and --produce-models used together (before it... 
X-Git-Tag: cvc5-1.0.0~6735
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=55ca82cf4c48911e7cdad7f82b58497ba9822579;p=cvc5.git

Fatal error if --unconstrained-simp and --produce-models used together (before it would just override the user and turn off models).
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ffe239e2f..8938cd769 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1064,14 +1064,23 @@ void SmtEngine::setDefaults() {
   // Unconstrained simp currently does *not* support model generation
   if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp()) {
     if (options::produceModels()) {
+      if (options::produceModels.wasSetByUser()) {
+        throw OptionException("Cannot use unconstrained-simp with model generation.");
+      }
       Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << endl;
       setOption("produce-models", SExpr("false"));
     }
     if (options::produceAssignments()) {
+      if (options::produceAssignments.wasSetByUser()) {
+        throw OptionException("Cannot use unconstrained-simp with model generation (produce-assignments).");
+      }
       Notice() << "SmtEngine: turning off produce-assignments to support unconstrainedSimp" << endl;
       setOption("produce-assignments", SExpr("false"));
     }
     if (options::checkModels()) {
+      if (options::checkModels.wasSetByUser()) {
+        throw OptionException("Cannot use unconstrained-simp with model generation (check-models).");
+      }
       Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << endl;
       setOption("check-models", SExpr("false"));
     }
diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am
index dcc44d43a..a262499b8 100644
--- a/test/regress/regress0/unconstrained/Makefile.am
+++ b/test/regress/regress0/unconstrained/Makefile.am
@@ -13,7 +13,8 @@ TESTS_ENVIRONMENT = \
 	$(AM_LOG_FLAGS) $(LOG_FLAGS)
 endif
 
-override CVC4_REGRESSION_ARGS += --unconstrained-simp
+# models not supported with unconstrained simp
+override CVC4_REGRESSION_ARGS += --unconstrained-simp --no-check-models
 export CVC4_REGRESSION_ARGS
 
 MAKEFLAGS = -k