From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 2 Aug 2019 03:11:08 +0000 (-0500)
Subject: Enable sygus logic when produce-abducts is true (#3144)
X-Git-Tag: cvc5-1.0.0~4056
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0f32fff652b6bac70cc18fbaa49f922ca27c58e6;p=cvc5.git

Enable sygus logic when produce-abducts is true (#3144)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 709df6c9f..df46fc924 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1260,13 +1260,8 @@ void SmtEngine::setDefaults() {
   // sygus inference may require datatypes
   if (!d_isInternalSubsolver)
   {
-    if (options::produceAbducts())
-    {
-      // we may invoke a sygus conjecture, hence we need options related to
-      // sygus
-      is_sygus = true;
-    }
-    if (options::sygusInference() || options::sygusRewSynthInput())
+    if (options::produceAbducts() || options::sygusInference()
+        || options::sygusRewSynthInput())
     {
       // since we are trying to recast as sygus, we assume the input is sygus
       is_sygus = true;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1b1f87bfc..2c65c7e14 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -546,6 +546,7 @@ set(regress_0_tests
   regress0/nl/very-easy-sat.smt2
   regress0/nl/very-simple-unsat.smt2
   regress0/options/invalid_dump.smt2
+  regress0/opt-abd-no-use.smt2
   regress0/parallel-let.smt2
   regress0/parser/as.smt2
   regress0/parser/bv_arity_smt2.6.smt2
diff --git a/test/regress/regress0/opt-abd-no-use.smt2 b/test/regress/regress0/opt-abd-no-use.smt2
new file mode 100644
index 000000000..65f1f3ae5
--- /dev/null
+++ b/test/regress/regress0/opt-abd-no-use.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_LIA)
+(set-info :status sat)
+(set-option :produce-abducts true)
+(declare-fun x () Int)
+(assert (> x 0))
+(check-sat)