diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-08-24 00:29:52 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-08-24 00:29:52 +0000 |
| commit | 9de66957df6448ba1243cdb7cc84813fe82e69d5 (patch) | |
| tree | 9c013455d7f0c0e057f44f51abdead7ff1ebd01c /src/expr/expr_template.cpp | |
| parent | 23367b1eac54a17a060697b1cf187ad2cc2ff503 (diff) | |
fix get-value output in a couple ways; this fixes bug #378
Diffstat (limited to 'src/expr/expr_template.cpp')
| -rw-r--r-- | src/expr/expr_template.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index f88914fd2..b0364348c 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -168,7 +168,7 @@ Debug("export") << "+ child: " << *i << std::endl; }/* CVC4::expr namespace */ -Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { +Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) const { Assert(d_exprManager != exprManager, "No sense in cloning an Expr in the same ExprManager"); ExprManagerScope ems(*this); |