From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 9 Dec 2019 22:17:46 +0000 (-0600)
Subject: Disable sygus inference when combined with incremental and proofs (#3539)
X-Git-Tag: cvc5-1.0.0~3780
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2b4e146c3a090e21b64d48ebb4308e5ec58a8c4b;p=cvc5.git

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