Fix spurious assertion for trivial abduction (#6629)

Fixes 2nd benchmark from #6605.

1 files changed, 14 insertions, 12 deletions

diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index 6be05c6b7..ff1337fe1 100644
--- 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())