diff options
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
| -rw-r--r-- | src/expr/expr_manager_template.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 84f674d2b..ef74575f3 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -941,6 +941,11 @@ Expr ExprManager::mkBoundVar(Type type) { return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode)); } +Expr ExprManager::mkSepNil(Type type) { + NodeManagerScope nms(d_nodeManager); + return Expr(this, d_nodeManager->mkSepNilPtr(*type.d_typeNode)); +} + Expr ExprManager::mkAssociative(Kind kind, const std::vector<Expr>& children) { PrettyCheckArgument( |