diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-14 17:03:44 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-14 17:03:44 -0500 |
commit | 08d6ec676189826f99756f9245186ee9de7dbc36 (patch) | |
tree | 0705bfd0caf37d694c87b7a907edcd5bea466cbe /src/expr/expr_template.cpp | |
parent | 9d7766ed1e41da53d59ad16e9ef8be8f522226df (diff) |
Fix bug related to portfolio with nullary operators.
Diffstat (limited to 'src/expr/expr_template.cpp')
-rw-r--r-- | src/expr/expr_template.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 4fbb0cd33..806650e57 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -137,7 +137,12 @@ public: return to->mkConst(::CVC4::EmptySet(type)); } return exportConstant(n, NodeManager::fromExprManager(to), vmap); - } else if(n.isVar()) { + } else if(n.getMetaKind() == metakind::NULLARY_OPERATOR ){ + Expr from_e(from, new Node(n)); + Type type = from->exportType(from_e.getType(), to, vmap); + NodeManagerScope nullScope(NULL); + return to->mkNullaryOperator(type, n.getKind()); // FIXME thread safety + } else if(n.getMetaKind() == metakind::VARIABLE) { Expr from_e(from, new Node(n)); Expr& to_e = vmap.d_typeMap[from_e]; if(! to_e.isNull()) { |