enable new code path for mod handling

Z3Prover · Aug 17, 2022 · 1a5503c · 1a5503c
1 parent cb272bd
commit 1a5503c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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);