fix #4871

src/tactic/core/solve_eqs_tactic.cpp

@@ -321,23 +321,27 @@ class solve_eqs_tactic : public tactic {
 
         bool solve_mod(expr * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) {
             rational r1, r2;
-            expr* arg1, *arg2, *arg3, *arg4;
-            if (m_produce_proofs) {
-                return false;
-            }
-            VERIFY(m_a_util.is_mod(lhs, arg1, arg2));
-            if (!m_a_util.is_numeral(arg2, r1) || !r1.is_pos()) {
+            expr* arg1;
+            if (m_produce_proofs) 
                 return false;
-            }
-            if (m_a_util.is_mod(rhs, arg3, arg4) && m_a_util.is_numeral(arg4, r2) && r1 == r2) {
-                rhs = arg3;
-            }
-            else if (!m_a_util.is_numeral(rhs, r2) || !r2.is_zero()) {
+
+            auto fresh = [&]() { return m().mk_fresh_const("mod", m_a_util.mk_int()); };
+            auto mk_int = [&](rational const& r) { return m_a_util.mk_int(r); };
+            auto add = [&](expr* a, expr* b) { return m_a_util.mk_add(a, b); };
+            auto mul = [&](expr* a, expr* b) { return m_a_util.mk_mul(a, b); };
+
+            VERIFY(m_a_util.is_mod(lhs, lhs, arg1));
+            if (!m_a_util.is_numeral(arg1, r1) || !r1.is_pos()) {
                 return false;
             }
-            if (solve_eq(arg1, rhs, eq, var, def, pr)) {
-                def = m_a_util.mk_add(def, m_a_util.mk_mul(m().mk_fresh_const("mod", m_a_util.mk_int()), m_a_util.mk_int(r1)));
-                return true;
+            // 
+            // solve lhs mod r1 = r2
+            // as lhs = r1*mod!1 + r2
+            // 
+            if (m_a_util.is_numeral(rhs, r2) && r2 < r1) {
+                expr_ref def0(m());
+                def0 = add(mk_int(r2), mul(fresh(), mk_int(r1)));
+                return solve_eq(lhs, def0, eq, var, def, pr);
             }
             return false;
         }