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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 709df6c9f031c067e4cebb35cb31d861c33b3388..df46fc924460794701896c8fa535351ee4e4ec54 100644 (file)
--- 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 1b1f87bfcfcd8add12d2252c643c18d7b99b3db3..2c65c7e140b3e20991cc5662f8bdbfc4608748b0 100644 (file)
--- 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 (file)
index 0000000..65f1f3a
--- /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)