diff options
Diffstat (limited to 'src')
-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; |