diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-08 22:31:44 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-08 22:31:44 +0000 |
commit | 480d440174c565bec9aba412c0d35221c9169ff6 (patch) | |
tree | 12048b5ba5d9717d6770b5d89de23d9c7048a981 /src/expr/expr_template.cpp | |
parent | cfa9e2cbbdf77a325791b5548b41093a0781311c (diff) |
Some minor changes after reviewing the portfolio "unified driver" commit.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/expr/expr_template.cpp')
-rw-r--r-- | src/expr/expr_template.cpp | 8 |
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(); } |