diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
index 27e77bd29..994efcb42 100644
--- a/src/qe/mbp/mbp_arith.cpp
+++ b/src/qe/mbp/mbp_arith.cpp
@@ -214,7 +214,7 @@ namespace mbp {
                     throw default_exception("mbp evaluation didn't produce a truth value");
                 }
             }
-            else if (false && a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && mul1 > 0) {
+            else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && mul1 > 0) {
                 // v = t1 mod mul1
                 vars coeffs;
                 rational c0 = add_def(t1, mul1, coeffs);