diff options
Diffstat (limited to 'src/smt/interpolation_solver.cpp')
-rw-r--r-- | src/smt/interpolation_solver.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 813fc45cf..fbbdb1b90 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -19,11 +19,13 @@ #include "base/modal_exception.h" #include "options/smt_options.h" +#include "smt/env.h" #include "smt/smt_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_interpol.h" #include "theory/smt_engine_subsolver.h" +#include "theory/trust_substitutions.h" using namespace cvc5::theory; @@ -50,7 +52,7 @@ bool InterpolationSolver::getInterpol(const Node& conj, << std::endl; std::vector<Node> axioms = d_parent->getExpandedAssertions(); // must expand definitions - Node conjn = d_parent->expandDefinitions(conj); + Node conjn = d_parent->getEnv().getTopLevelSubstitutions().apply(conj); std::string name("A"); quantifiers::SygusInterpol interpolSolver; |