Some fixes to portfolio

[cvc5.git] / src / expr / expr_template.cpp

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index f39c0e7eadcc714c53f89c9be98373ad923bf84f..2f9e27c0c0309981a32eebb0e21cbeba27e0226f 100644 (file)
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -114,7 +114,12 @@ namespace expr {
 static Node exportConstant(TNode n, NodeManager* to);
 
 Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap) {
-  if(n.isConst()) {
+  if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
+    throw ExportUnsupportedException
+       ("export of node belonging to theory of DATATYPES kinds unsupported");
+  }
+
+  if(n.getMetaKind() == metakind::CONSTANT) {
     return exportConstant(n, NodeManager::fromExprManager(to));
   } else if(n.isVar()) {
     Expr from_e(from, new Node(n));
@@ -132,7 +137,7 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
         // a check that mkVar isn't called internally
         NodeManagerScope nullScope(NULL);
 
-        if(n.getKind() == kind::BOUND_VAR_LIST) {
+        if(n.getKind() == kind::BOUND_VAR_LIST || n.getKind() == kind::BOUND_VARIABLE) {
           to_e = to->mkBoundVar(name, type);// FIXME thread safety
         } else if(n.getKind() == kind::VARIABLE) {
           to_e = to->mkVar(name, type);// FIXME thread safety