Make interpolation robust to conjectures with no shared variables (#8840)

Fixes #8833.

diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index 1894c889cc08f3ac152a545827042c6b5f7fd391..8ce073b93fc488dc2bddac0a6c495ff34186803b 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -90,7 +90,10 @@ void SygusInterpol::createVariables(bool needsShared)
     }
   }
   // make the sygus variable list
-  d_ibvlShared = nm->mkNode(kind::BOUND_VAR_LIST, d_vlvsShared);
+  if (!d_vlvsShared.empty())
+  {
+    d_ibvlShared = nm->mkNode(kind::BOUND_VAR_LIST, d_vlvsShared);
+  }
   Trace("sygus-interpol-debug") << "...finish" << std::endl;
 }
 
@@ -234,12 +237,15 @@ void SygusInterpol::mkSygusConjecture(Node itp,
 
   // set the sygus bound variable list
   Trace("sygus-interpol-debug") << "Set attributes..." << std::endl;
-  itp.setAttribute(SygusSynthFunVarListAttribute(), d_ibvlShared);
+  if (!d_ibvlShared.isNull())
+  {
+    itp.setAttribute(SygusSynthFunVarListAttribute(), d_ibvlShared);
+  }
   Trace("sygus-interpol-debug") << "...finish" << std::endl;
 
   // Fa( x )
   Trace("sygus-interpol-debug") << "Make conjecture body..." << std::endl;
-  Node Fa = axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms);
+  Node Fa = nm->mkAnd(axioms);
   // Fa( x ) => A( x )
   Node firstImplication = nm->mkNode(kind::IMPLIES, Fa, itpApp);
   Trace("sygus-interpol-debug")

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 39d9d92bc397d6a1ba8705501fdbfe4791775f52..4ffe4421e1b907170726332c321d14cb7ac1ffaf 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -755,6 +755,7 @@ set(regress_0_tests
   regress0/issue6738.smt2
   regress0/issue6741.smt2
   regress0/issue8807-model-core-partial.smt2
+  regress0/issue8833-interpol-no-shared-var.smt2
   regress0/issue8834-model-core-nconst.smt2
   regress0/ite_arith.smt2
   regress0/ite_real_int_type.smtv1.smt2

diff --git a/test/regress/cli/regress0/issue8833-interpol-no-shared-var.smt2 b/test/regress/cli/regress0/issue8833-interpol-no-shared-var.smt2
new file mode 100644 (file)
index 0000000..758df00
--- /dev/null
+++ b/test/regress/cli/regress0/issue8833-interpol-no-shared-var.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: --produce-interpolants -q
+; EXPECT: fail
+(set-logic ALL)
+(declare-fun a () Int)
+(get-interpolant A (> a 0))