From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 27 May 2021 20:02:43 +0000 (-0500)
Subject: Fix spurious assertion for trivial abduction (#6629)
X-Git-Tag: cvc5-1.0.0~1686
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8d63f44d93ae91c5b89a9cf866ba33c954465398;p=cvc5.git

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 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())
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 817ddc2ba..81e5ca8c6 100644
--- 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
index 000000000..7eaaff6b5
--- /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)