From 2b4e146c3a090e21b64d48ebb4308e5ec58a8c4b Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 9 Dec 2019 16:17:46 -0600
Subject: [PATCH] Disable sygus inference when combined with incremental and
 proofs (#3539)

---
 src/smt/smt_engine.cpp | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c034f6f23..80296f400 100644
--- 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
   {
-- 
2.30.2