From f44197f3cce5a7005fa03dd64b812d4cf79d53bd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 4 Jun 2022 18:27:22 -0500 Subject: [PATCH] Fix corner case of interpolants from conjectures with no free variables (#8853) Fixes #8852. --- src/theory/quantifiers/sygus/sygus_interpol.cpp | 6 +++++- test/regress/cli/CMakeLists.txt | 1 + test/regress/cli/regress1/issue8852-interpol-no-var.smt2 | 6 ++++++ 3 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 test/regress/cli/regress1/issue8852-interpol-no-var.smt2 diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 8ce073b93..7230e0ce6 100644 --- 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 d13f8ba78..2e961af07 100644 --- 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 index 000000000..cf5e032ea --- /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)) -- 2.30.2