From 55ca82cf4c48911e7cdad7f82b58497ba9822579 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 20 Jun 2014 15:13:23 -0400
Subject: [PATCH] Fatal error if --unconstrained-simp and --produce-models used
 together (before it would just override the user and turn off models).

---
 src/smt/smt_engine.cpp                          | 9 +++++++++
 test/regress/regress0/unconstrained/Makefile.am | 3 ++-
 2 files changed, 11 insertions(+), 1 deletion(-)

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
-- 
2.30.2