diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/command.cpp | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 2 |
2 files changed, 1 insertions, 3 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 5fb4d1fbd..61702561a 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -338,7 +338,7 @@ Expr DefineFunctionCommand::getFormula() const { } void DefineFunctionCommand::invoke(SmtEngine* smtEngine) { - Dump("declarations") << *this << endl; + //Dump("declarations") << *this << endl; -- done by SmtEngine if(!d_func.isNull()) { smtEngine->defineFunction(d_func, d_formals, d_formula); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d11130aac..24ebf9bfd 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -409,7 +409,6 @@ void SmtEngine::defineFunction(Expr func, const std::vector<Expr>& formals, Expr formula) { Trace("smt") << "SMT defineFunction(" << func << ")" << endl; - /* if(Dump.isOn("declarations")) { stringstream ss; ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations"))) @@ -417,7 +416,6 @@ void SmtEngine::defineFunction(Expr func, Dump("declarations") << DefineFunctionCommand(ss.str(), func, formals, formula) << endl; } - */ NodeManagerScope nms(d_nodeManager); // type check body |