summaryrefslogtreecommitdiff
path: root/src/smt/boolean_terms.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/boolean_terms.cpp')
-rw-r--r--src/smt/boolean_terms.cpp3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index b3e69619f..80518fcdf 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -736,7 +736,8 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
k != kind::TUPLE_SELECT &&
k != kind::TUPLE_UPDATE &&
k != kind::RECORD_SELECT &&
- k != kind::RECORD_UPDATE) {
+ k != kind::RECORD_UPDATE &&
+ k != kind::DIVISIBLE) {
Debug("bt") << "rewriting: " << top.getOperator() << endl;
result.top() << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars);
Debug("bt") << "got: " << result.top().getOperator() << endl;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback