diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-14 07:33:01 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-14 09:33:01 -0500 |
| commit | c13527bfa6b47ff4675b429b5e7bb7c6f43ff595 (patch) | |
| tree | f182e942b3bc4ad99a8fdf765959781f1a2570dd /src/expr/expr_template.cpp | |
| parent | 1cd3c3c5dad84093aa6b2db164798c8fff473fec (diff) | |
Use TypeNode in EmptySet (#4740)
This commit changes EmptySet to use TypeNode instead of Type.
Diffstat (limited to 'src/expr/expr_template.cpp')
| -rw-r--r-- | src/expr/expr_template.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 132d4bfaa..226736e8f 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -181,8 +181,8 @@ private: if(n.getMetaKind() == metakind::CONSTANT) { if(n.getKind() == kind::EMPTYSET) { Type type = d_from->exportType( - n.getConst< ::CVC4::EmptySet>().getType(), d_to, d_vmap); - return d_to->mkConst(::CVC4::EmptySet(type)); + n.getConst< ::CVC4::EmptySet>().getType().toType(), d_to, d_vmap); + return d_to->mkConst(::CVC4::EmptySet(TypeNode::fromType(type))); } return exportConstant(n, NodeManager::fromExprManager(d_to), d_vmap); } else if(n.getMetaKind() == metakind::NULLARY_OPERATOR ){ |