From 1a5503c87b91897587a927c7ab45f0e66078a748 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 17 Aug 2022 07:31:20 -0700
Subject: [PATCH] enable new code path for mod handling

---
 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 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);