Fix corner case of interpolants from conjectures with no free variables (#8853)

Fixes #8852.

diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index 8ce073b93fc488dc2bddac0a6c495ff34186803b..7230e0ce6507777551e0f72efc073d52c448eccd 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -296,7 +296,11 @@ bool SygusInterpol::findInterpol(SolverEngine* subSolver,
 
   // get the grammar type for the interpolant
   Node igdtbv = itp.getAttribute(SygusSynthFunVarListAttribute());
-  Assert(!igdtbv.isNull());
+  // could have no variables, in which case there is nothing to do
+  if (igdtbv.isNull())
+  {
+    return true;
+  }
   Assert(igdtbv.getKind() == kind::BOUND_VAR_LIST);
   // convert back to original
   // must replace formal arguments of itp with the free variables in the

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index d13f8ba78d99f05b2fab9c9cc677db8a9c239091..2e961af07406c3c0430e30e585123484cf16bf5b 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1997,6 +1997,7 @@ set(regress_1_tests
   regress1/issue5739-rtf-processed.smt2
   regress1/issue7902-abd-subsolver-uc.smt2
   regress1/issue7937-difficulty-irr.smt2
+  regress1/issue8852-interpol-no-var.smt2
   regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
   regress1/lemmas/pursuit-safety-8.smtv1.smt2
   regress1/minimal_unsat_core.smt2

diff --git a/test/regress/cli/regress1/issue8852-interpol-no-var.smt2 b/test/regress/cli/regress1/issue8852-interpol-no-var.smt2
new file mode 100644 (file)
index 0000000..cf5e032
--- /dev/null
+++ b/test/regress/cli/regress1/issue8852-interpol-no-var.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --produce-interpolants
+; EXPECT: (define-fun A () Bool false)
+(set-logic ALL)
+(declare-fun a () Int)
+(assert (<= 1 0))
+(get-interpolant A (> a 0))