diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-22 14:07:21 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-22 14:07:28 -0500 |
commit | 0ee7aa783c299eca1127005b590dd157b315f130 (patch) | |
tree | 23d95924956b6bdcfc9a7bc9b6996ac00657007e /src/smt | |
parent | 5d600cd2df87f81ec19034a79e7fe4eea9482b4c (diff) |
Bug fix for define functions + incremental. Minor work on relational triggers.
Diffstat (limited to 'src/smt')
-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()); |