Fix bug related to portfolio with nullary operators.

2 files changed, 9 insertions, 4 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()) {
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 7cf228403..e9e92a5b1 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -459,7 +459,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
   /* The check should have happened, if we asked for it. */
   Assert( !check || getAttribute(n, TypeCheckedAttr()) );
 
-  Debug("getType") << "type of " << n << " is " << typeNode << endl;
+  Debug("getType") << "type of " << &n << " " <<  n << " is " << typeNode << endl;
   return typeNode;
 }
 
@@ -799,10 +799,10 @@ Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) {
     //setAttribute(n, TypeCheckedAttr(), true);
     d_unique_vars[k][type] = n;
     Assert( n.getMetaKind() == kind::metakind::NULLARY_OPERATOR );
-    Trace("ajr-temp") << this << "...made nullary operator " << n << std::endl;
+    Trace("ajr-temp") << this << "...made nullary operator " << n << " " << &n << " " << type << std::endl;
     return n;
   }else{
-    Trace("ajr-temp") << this << "...reuse nullary operator " << it->second << std::endl;
+    Trace("ajr-temp") << this << "...reuse nullary operator " << it->second << " " << &( it->second ) << std::endl;
     return it->second;
   }
 }