Some minor changes after reviewing the portfolio "unified driver" commit.

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 5 insertions, 3 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 4009bc610..08c3a2b1e 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -137,9 +137,11 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
         } else if(n.getKind() == kind::VARIABLE) {
           to_e = to->mkVar(name, type);// FIXME thread safety
         } else if(n.getKind() == kind::SKOLEM) {
-          Assert(false, "Skolem exporting not yet supported properly.");
-          // to fix this, get the node manager and do the appropriate
-          to_e = to->mkVar(name, type);// FIXME thread safety
+          // skolems are only available at the Node level (not the Expr level)
+          TypeNode typeNode = TypeNode::fromType(type);
+          NodeManager* to_nm = NodeManager::fromExprManager(to);
+          Node n = to_nm->mkSkolem(name, typeNode);// FIXME thread safety
+          to_e = n.toExpr();
         } else {
           Unhandled();
         }