From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 10 Dec 2019 15:07:47 +0000 (-0600)
Subject: Allow unsat cores with sygus inference (#3550)
X-Git-Tag: cvc5-1.0.0~3779
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ee5fed52332ec6baddc8ecd8f8e04a644990bf29;p=cvc5.git

Allow unsat cores with sygus inference (#3550)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 80296f400..0276684d6 100644
--- 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 0a2f3feaa..08f929c4c 100644
--- 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))