Fix bug related to portfolio with nullary operators.

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()) {