Fatal error if --unconstrained-simp and --produce-models used together (before it...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ffe239e2f21be16afbb4f033eae7147b4e149a52..8938cd769ed36b198a9360062fe945ac5df4d328 100644 (file)
--- 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 dcc44d43aae82f8f2503f208ea530876df7d2c9a..a262499b866b6d07b0e7b9b732c4146d3e7ccc68 100644 (file)
--- 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