diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5e97158ca..bbaa07af5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2123,6 +2123,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const void SmtEngine::defineFunction(Expr func, const std::vector<Expr>& formals, Expr formula) { + SmtScope smts(this); + doPendingPops(); Trace("smt") << "SMT defineFunction(" << func << ")" << endl; for(std::vector<Expr>::const_iterator i = formals.begin(); i != formals.end(); ++i) { if((*i).getKind() != kind::BOUND_VARIABLE) { @@ -2141,7 +2143,6 @@ void SmtEngine::defineFunction(Expr func, DefineFunctionCommand c(ss.str(), func, formals, formula); addToModelCommandAndDump(c, ExprManager::VAR_FLAG_DEFINED, true, "declarations"); - SmtScope smts(this); PROOF( if (options::checkUnsatCores()) { d_defineCommands.push_back(c.clone()); |