enable nested division

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Aug 15, 2022 · 583dae2 · 583dae2
1 parent 681ed95
commit 583dae2
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
@@ -234,7 +234,7 @@ namespace mbp {
                 rational c0 = add_def(t1, mul1, coeffs);
                 tids.insert(t, mbo.add_mod(coeffs, c0, mul1));
             }
-            else if (false && a.is_idiv(t, t1, t2) && is_numeral(t2, mul1) && mul1 > 0) {
+            else if (a.is_idiv(t, t1, t2) && is_numeral(t2, mul1) && mul1 > 0) {
                 // v = t1 div mul1
                 vars coeffs;
                 rational c0 = add_def(t1, mul1, coeffs);