diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-09-12 14:44:49 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-09-12 14:44:49 -0400 |
commit | 470c20cd7d12f8de3e9d4e7c38d2ebba1296b098 (patch) | |
tree | eba01503e16a20ac5eb1f4e44e7f87aa4b16acbd /src/expr/command.cpp | |
parent | 28ec8ce392a815c47689ecd86b5b91f9a58104e5 (diff) |
fix bug 534: portfolio define-fun duplicate model
Diffstat (limited to 'src/expr/command.cpp')
-rw-r--r-- | src/expr/command.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index d0bd02c8a..8ae448657 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -467,6 +467,7 @@ Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapColle Command* cmd_to_export = *i; Command* cmd = cmd_to_export->exportTo(exprManager, variableMap); seq->addCommand(cmd); + Debug("export") << "[export] so far coverted: " << seq << endl; } seq->d_index = d_index; return seq; @@ -671,7 +672,7 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { } Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - Expr func = d_func.exportTo(exprManager, variableMap); + Expr func = d_func.exportTo(exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED); vector<Expr> formals; transform(d_formals.begin(), d_formals.end(), back_inserter(formals), ExportTransformer(exprManager, variableMap)); |