Fix spurious assertion for trivial abduction (#6629)

Fixes 2nd benchmark from #6605.

diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index 6be05c6b7e8de57ec20fb7e470440e1de4c455d7..ff1337fe1fbe6dec897c25739803a6ffddf51a53 100644 (file)
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -105,20 +105,22 @@ bool AbductionSolver::getAbductInternal(Node& abd)
       }
       // get the grammar type for the abduct
       Node agdtbv = d_sssf.getAttribute(SygusSynthFunVarListAttribute());
-      Assert(!agdtbv.isNull());
-      Assert(agdtbv.getKind() == kind::BOUND_VAR_LIST);
-      // convert back to original
-      // must replace formal arguments of abd with the free variables in the
-      // input problem that they correspond to.
-      std::vector<Node> vars;
-      std::vector<Node> syms;
-      SygusVarToTermAttribute sta;
-      for (const Node& bv : agdtbv)
+      if(!agdtbv.isNull())
       {
-        vars.push_back(bv);
-        syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv);
+        Assert(agdtbv.getKind() == kind::BOUND_VAR_LIST);
+        // convert back to original
+        // must replace formal arguments of abd with the free variables in the
+        // input problem that they correspond to.
+        std::vector<Node> vars;
+        std::vector<Node> syms;
+        SygusVarToTermAttribute sta;
+        for (const Node& bv : agdtbv)
+        {
+          vars.push_back(bv);
+          syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv);
+        }
+        abd = abd.substitute(vars.begin(), vars.end(), syms.begin(), syms.end());
       }
-      abd = abd.substitute(vars.begin(), vars.end(), syms.begin(), syms.end());
 
       // if check abducts option is set, we check the correctness
       if (options::checkAbducts())

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 817ddc2ba6e9d855fa35cb0810b357456f41859e..81e5ca8c64518f864307f3fd7bcf9a54392337b0 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -660,6 +660,7 @@ set(regress_0_tests
   regress0/issue5540-2-dump-model.smt2
   regress0/issue5540-model-decls.smt2
   regress0/issue5550-num-children.smt2
+  regress0/issue6605-2-abd-triv.smt2
   regress0/ite_arith.smt2
   regress0/ite_real_int_type.smtv1.smt2
   regress0/ite_real_valid.smtv1.smt2

diff --git a/test/regress/regress0/issue6605-2-abd-triv.smt2 b/test/regress/regress0/issue6605-2-abd-triv.smt2
new file mode 100644 (file)
index 0000000..7eaaff6
--- /dev/null
+++ b/test/regress/regress0/issue6605-2-abd-triv.smt2
@@ -0,0 +1,4 @@
+; COMMAND-LINE: --produce-abducts
+; EXPECT: (define-fun A () Bool true)
+(set-logic ALL)
+(get-abduct A true)