1 files changed, 5 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index dd8a2e502..029fb84c9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1481,8 +1481,11 @@ void SmtEngine::setDefaults() {
     options::boolToBitvector.set(false);
   }
 
-  if(options::produceAssignments() && !options::produceModels()) {
-    Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl;
+  // cases where we need produce models
+  if (!options::produceModels()
+      && (options::produceAssignments() || options::sygusRewSynthCheck()))
+  {
+    Notice() << "SmtEngine: turning on produce-models" << endl;
     setOption("produce-models", SExpr("true"));
   }