Fix spurious assertion for trivial abduction (#6629)

Fixes 2nd benchmark from #6605.
cvc5 · May 27, 2021 · 8d63f44 · 8d63f44
1 parent c95d4c5
commit 8d63f44
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 12 deletions.
diff --git 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
@@ -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
@@ -0,0 +1,4 @@
+; COMMAND-LINE: --produce-abducts
+; EXPECT: (define-fun A () Bool true)
+(set-logic ALL)
+(get-abduct A true)