From 583dae2e272d194a5f3204294d4d7b0d142b8774 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Aug 2022 16:11:00 -0700 Subject: [PATCH] enable nested division Signed-off-by: Nikolaj Bjorner --- src/qe/mbp/mbp_arith.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index 713a63c1447..950a92fb50f 100644 --- 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);