Disable sygus inference when combined with incremental and proofs (#3539)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c034f6f2345e03ff73e942bd3f5132f6d3330314..80296f40039a227b71fd54ebcd4459000da83914 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1338,6 +1338,19 @@ 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
   {