diff options
Diffstat (limited to 'src/smt/term_formula_removal.cpp')
| -rw-r--r-- | src/smt/term_formula_removal.cpp | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 250c21202..fc10d2b4b 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -215,8 +215,11 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output, // The representation is now the skolem return skolem; } - - if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + + if (node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS + || node.getKind() == kind::LAMBDA + || node.getKind() == kind::CHOICE) + { // Remember if we're inside a quantifier inQuant = true; }else if( !inTerm && hasNestedTermChildren( node ) ){ @@ -275,7 +278,10 @@ Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const { return cached.isNull() ? Node(node) : cached; } - if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + if (node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS + || node.getKind() == kind::LAMBDA + || node.getKind() == kind::CHOICE) + { // Remember if we're inside a quantifier inQuant = true; }else if( !inTerm && hasNestedTermChildren( node ) ){ |