diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-21 00:20:07 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-21 00:20:07 -0700 |
| commit | 839f71ec5496d6fdfee5a7ad0e96e282cbcd0311 (patch) | |
| tree | 7b3385ec2193067cd6e6993720b23dcf172fc11d | |
| parent | 306c31799bcc67da2db43aa20ee714aff21e43c0 (diff) | |
minor
| -rw-r--r-- | src/expr/node_manager.h | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 8962b1cfa..e99c70f7c 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -490,10 +490,6 @@ class NodeManager /** Create a node with three children by operator. */ Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3); - /** Create a node with four children by operator. */ - Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3, - TNode child4); - /** Create a node by applying an operator to the children. */ template <bool ref_count> Node mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children); |