diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-28 22:22:05 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-28 22:22:05 -0500 |
| commit | 233f056a68c34eebdd6c349ac74e9708437c4b27 (patch) | |
| tree | 17ef7adec0c2570219a71126350e2ebf51b6066b /src/smt/term_formula_removal.cpp | |
| parent | 3d1ad64367948039f67f653e34f19359e3c9c496 (diff) | |
Fix bug 787.
Diffstat (limited to 'src/smt/term_formula_removal.cpp')
| -rw-r--r-- | src/smt/term_formula_removal.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 3fd333cc5..87db183e2 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -155,7 +155,8 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output, inQuant = true; }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR && - node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL ){ + node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL && + node.getKind()!=kind::BITVECTOR_EAGER_ATOM ){ // Remember if we're inside a term Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl; inTerm = true; |