diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-12 12:23:57 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-12 12:23:57 -0500 |
commit | af135825a60f917711d133828c9fdd6831e2142d (patch) | |
tree | 20e9b46a027b8f8242901964fa360bb849f640df /src/smt | |
parent | 6b5b926f28b66c3812d77fd234e93b9eee03f71f (diff) |
Fixes for free variables in assertions (#1762)
Diffstat (limited to 'src/smt')
-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 ) ){ |