From c3d635cf77a17e9d512f0ccdb7db85c64ad47e47 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Aug 2022 12:50:30 -0700 Subject: [PATCH] handle build warning Signed-off-by: Nikolaj Bjorner --- src/qe/mbp/mbp_arith.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index 994efcb42..9a9a6f79d 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -494,7 +494,8 @@ namespace mbp { if (r.m_type == opt::t_div) continue; - if (r.m_vars.size() == 1 && r.m_vars[0].m_coeff.is_neg() && r.m_type != opt::t_divides) { + if (r.m_vars.size() == 1 && r.m_vars[0].m_coeff.is_neg() && + (r.m_type == opt::t_eq || r.m_type == opt::t_le || r.m_type == opt::t_lt)) { var const& v = r.m_vars[0]; t = id2expr(def_vars, index2expr, v.m_id); if (!v.m_coeff.is_minus_one()) { @@ -505,7 +506,7 @@ namespace mbp { case opt::t_lt: t = a.mk_gt(t, s); break; case opt::t_le: t = a.mk_ge(t, s); break; case opt::t_eq: t = a.mk_eq(t, s); break; - default: UNREACHABLE(); + default: UNREACHABLE(); break; } fmls.push_back(t); continue; @@ -519,6 +520,9 @@ namespace mbp { case opt::t_divides: t = a.mk_eq(a.mk_mod(t, a.mk_int(r.m_mod)), a.mk_int(0)); break; + default: + UNREACHABLE(); + break; } fmls.push_back(t); }