From 249f0de80b68c0bf203f8f8492256d9c81fadb14 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 26 Jul 2023 10:06:41 -0700 Subject: [PATCH] fix order for inequalities in arithmetic justifications such that implied bound literal is last. The self-checker uses this property to identify the implied bound Signed-off-by: Nikolaj Bjorner --- src/sat/smt/arith_diagnostics.cpp | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp index bdcddc03d..77c51d87c 100644 --- a/src/sat/smt/arith_diagnostics.cpp +++ b/src/sat/smt/arith_diagnostics.cpp @@ -209,12 +209,6 @@ namespace arith { rational lc(1); for (unsigned i = m_lit_head; i < m_lit_tail; ++i) lc = lcm(lc, denominator(a.m_arith_hint.lit(i).first)); - - for (unsigned i = m_lit_head; i < m_lit_tail; ++i) { - auto const& [coeff, lit] = a.m_arith_hint.lit(i); - args.push_back(arith.mk_int(abs(coeff*lc))); - args.push_back(s.literal2expr(lit)); - } for (unsigned i = m_eq_head; i < m_eq_tail; ++i) { auto [x, y, is_eq] = a.m_arith_hint.eq(i); if (x->get_id() > y->get_id()) @@ -224,6 +218,11 @@ namespace arith { args.push_back(arith.mk_int(1)); args.push_back(eq); } + for (unsigned i = m_lit_head; i < m_lit_tail; ++i) { + auto const& [coeff, lit] = a.m_arith_hint.lit(i); + args.push_back(arith.mk_int(abs(coeff*lc))); + args.push_back(s.literal2expr(lit)); + } return m.mk_app(symbol(name), args.size(), args.data(), m.mk_proof_sort()); } }