From 2dac76d19ac5327d0f7047a368f06dd92f7f08bd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 27 Feb 2026 13:07:39 -1000 Subject: [PATCH] Handle overflow predicates in new core bit-vector internalization Add internalize_overflow() to handle OP_BUMUL_OVFL, OP_BSMUL_OVFL, OP_BUADD_OVFL, OP_BSADD_OVFL, OP_BUSUB_OVFL, OP_BSSUB_OVFL, OP_BSDIV_OVFL, and OP_BNEG_OVFL in the sat.euf=true solver path. Previously these overflow predicates hit UNREACHABLE() in internalize_circuit(). Now they are reduced to equivalent expressions using existing BV operations and internalized via add_def(). Fixes the assertion violation from #7027 for bvuaddo and related overflow predicates with tactic.default_tactic=smt sat.euf=true. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/sat/smt/bv_internalize.cpp | 89 ++++++++++++++++++++++++++++++++++ src/sat/smt/bv_solver.h | 1 + 2 files changed, 90 insertions(+) diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index e8ead7704..61ef8df72 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -202,6 +202,14 @@ namespace bv { case OP_BUMUL_NO_OVFL: internalize_nfl(mk_umul_no_overflow); break; case OP_BSMUL_NO_OVFL: internalize_nfl(mk_smul_no_overflow); break; case OP_BSMUL_NO_UDFL: internalize_nfl(mk_smul_no_underflow); break; + case OP_BUMUL_OVFL: + case OP_BSMUL_OVFL: + case OP_BSDIV_OVFL: + case OP_BNEG_OVFL: + case OP_BUADD_OVFL: + case OP_BSADD_OVFL: + case OP_BUSUB_OVFL: + case OP_BSSUB_OVFL: internalize_overflow(a); break; case OP_BIT2BOOL: internalize_bit2bool(a); break; case OP_ULEQ: internalize_le(a); break; case OP_SLEQ: internalize_le(a); break; @@ -613,6 +621,87 @@ namespace bv { add_clause(def, ~l); } + void solver::internalize_overflow(app* n) { + expr_ref def_expr(m); + expr* arg0 = n->get_arg(0); + + switch (n->get_decl_kind()) { + case OP_BUMUL_OVFL: { + expr_ref no_ovfl(bv.mk_bvumul_no_ovfl(arg0, n->get_arg(1)), m); + def_expr = m.mk_not(no_ovfl); + break; + } + case OP_BSMUL_OVFL: { + expr* arg1 = n->get_arg(1); + expr_ref no_ovfl(bv.mk_bvsmul_no_ovfl(arg0, arg1), m); + expr_ref no_udfl(bv.mk_bvsmul_no_udfl(arg0, arg1), m); + def_expr = m.mk_or(m.mk_not(no_ovfl), m.mk_not(no_udfl)); + break; + } + case OP_BUADD_OVFL: { + unsigned sz = bv.get_bv_size(arg0); + expr_ref a_ext(bv.mk_zero_extend(1, arg0), m); + expr_ref b_ext(bv.mk_zero_extend(1, n->get_arg(1)), m); + expr_ref sum(bv.mk_bv_add(a_ext, b_ext), m); + expr_ref carry(bv.mk_extract(sz, sz, sum), m); + expr_ref one(bv.mk_one(1), m); + def_expr = m.mk_eq(carry.get(), one.get()); + break; + } + case OP_BSADD_OVFL: { + unsigned sz = bv.get_bv_size(arg0); + expr* arg1 = n->get_arg(1); + expr_ref zero(bv.mk_zero(sz), m); + expr_ref sum(bv.mk_bv_add(arg0, arg1), m); + expr_ref a_pos(bv.mk_slt(zero, arg0), m); + expr_ref b_pos(bv.mk_slt(zero, arg1), m); + expr_ref sum_npos(bv.mk_sle(sum, zero), m); + expr_ref overflow(m.mk_and(a_pos, b_pos, sum_npos), m); + expr_ref a_neg(bv.mk_slt(arg0, zero), m); + expr_ref b_neg(bv.mk_slt(arg1, zero), m); + expr_ref sum_nneg(bv.mk_sle(zero, sum), m); + expr_ref underflow(m.mk_and(a_neg, b_neg, sum_nneg), m); + def_expr = m.mk_or(overflow, underflow); + break; + } + case OP_BUSUB_OVFL: { + expr_ref ule(bv.mk_ule(n->get_arg(1), arg0), m); + def_expr = m.mk_not(ule); + break; + } + case OP_BSSUB_OVFL: { + unsigned sz = bv.get_bv_size(arg0); + expr* arg1 = n->get_arg(1); + expr_ref minSigned(bv.mk_numeral(rational::power_of_two(sz - 1), sz), m); + expr_ref neg_b(bv.mk_bv_neg(arg1), m); + expr_ref saddo(bv.mk_bvsadd_ovfl(arg0, neg_b), m); + expr_ref zero(bv.mk_zero(sz), m); + expr_ref a_geq_zero(bv.mk_sle(zero, arg0), m); + expr_ref b_is_min(m.mk_eq(arg1, minSigned.get()), m); + def_expr = m.mk_ite(b_is_min, a_geq_zero, saddo); + break; + } + case OP_BSDIV_OVFL: { + unsigned sz = bv.get_bv_size(arg0); + expr_ref minSigned(bv.mk_numeral(rational::power_of_two(sz - 1), sz), m); + expr_ref minusOne(bv.mk_numeral(rational::power_of_two(sz) - 1, sz), m); + def_expr = m.mk_and(m.mk_eq(arg0, minSigned.get()), m.mk_eq(n->get_arg(1), minusOne.get())); + break; + } + case OP_BNEG_OVFL: { + unsigned sz = bv.get_bv_size(arg0); + expr_ref minSigned(bv.mk_numeral(rational::power_of_two(sz - 1), sz), m); + def_expr = m.mk_eq(arg0, minSigned.get()); + break; + } + default: + UNREACHABLE(); + } + + sat::literal def = ctx.internalize(def_expr, false, false); + add_def(def, expr2literal(n)); + } + void solver::internalize_concat(app* n) { euf::enode* e = expr2enode(n); theory_var v = e->get_th_var(get_id()); diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index e059fd12f..71019981e 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -286,6 +286,7 @@ namespace bv { void internalize_extract(app* n); void internalize_repeat(app* n); void internalize_bit2bool(app* n); + void internalize_overflow(app* n); void internalize_udiv_i(app* n); template void internalize_le(app* n);