Allow unsat cores with sygus inference (#3550)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 80296f40039a227b71fd54ebcd4459000da83914..0276684d68e2faa96675b88486617508ce4b0b41 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1338,19 +1338,6 @@ void SmtEngine::setDefaults() {
                << endl;
       options::unconstrainedSimp.set(false);
     }
-    if (options::sygusInference())
-    {
-      if (options::sygusInference.wasSetByUser())
-      {
-        throw OptionException(
-            "sygus inference not supported with unsat cores/proofs/incremental "
-            "solving");
-      }
-      Notice() << "SmtEngine: turning off sygus inference to support unsat "
-                  "cores/proofs/incremental solving"
-               << std::endl;
-      options::sygusInference.set(false);
-    }
   }
   else
   {
@@ -1371,6 +1358,22 @@ void SmtEngine::setDefaults() {
     }
   }
 
+  if (options::incrementalSolving() || options::proof())
+  {
+    if (options::sygusInference())
+    {
+      if (options::sygusInference.wasSetByUser())
+      {
+        throw OptionException(
+            "sygus inference not supported with proofs/incremental solving");
+      }
+      Notice() << "SmtEngine: turning off sygus inference to support "
+                  "proofs/incremental solving"
+               << std::endl;
+      options::sygusInference.set(false);
+    }
+  }
+
   // Disable options incompatible with unsat cores and proofs or output an
   // error if enabled explicitly
   if (options::unsatCores() || options::proof())

diff --git a/test/regress/regress1/quantifiers/issue3537.smt2 b/test/regress/regress1/quantifiers/issue3537.smt2
index 0a2f3feaab88ea4348d5fed7abf5dc5d89542ee7..08f929c4c3df8ef9db7bca429556e46904b3c653 100644 (file)
--- a/test/regress/regress1/quantifiers/issue3537.smt2
+++ b/test/regress/regress1/quantifiers/issue3537.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp
+; COMMAND-LINE: --strings-exp --no-check-models
 ; EXPECT: sat
 (set-logic ALL)
 (declare-datatypes ((UNIT 0)) (((Unit))