diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-14 01:45:58 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-14 10:45:58 +0200 |
| commit | 292b2c5712ce31282ac3ec564f268ee7f0aa3506 (patch) | |
| tree | 7333ca654b5716f5829a5c8bb00e7f7f98d1db08 /src/expr/expr_template.cpp | |
| parent | 88adf5e1416fb0c533fe3a24da5fce50aa5a2c0b (diff) | |
exportTo only if needed for --sygus-rr-synth-check (#2168)
Diffstat (limited to 'src/expr/expr_template.cpp')
| -rw-r--r-- | src/expr/expr_template.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 1344935af..3a0d31b2d 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -248,8 +248,11 @@ public: children.push_back(exportInternal(*i)); } if(Debug.isOn("export")) { - ExprManagerScope ems(*to); Debug("export") << "children for export from " << n << std::endl; + + // `n` belongs to the `from` ExprManager, so begin ExprManagerScope + // after printing `n` + ExprManagerScope ems(*to); for(std::vector<Node>::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) { Debug("export") << " child: " << *i << std::endl; } |