From 6eeb0220483c8693cdabe21e616f54fb751b669b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Mar 2024 16:00:09 -0700 Subject: [PATCH] fix encoding for sdiv exposed by zQkAOXjEDwgm Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat_internalize.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 7b65d3d01..8e3c08ce0 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -473,8 +473,8 @@ namespace polysat { rational N = rational::power_of_two(bv.get_bv_size(x)); expr_ref signx = mk_ule(bv.mk_numeral(N / 2, sz), x); expr_ref signy = mk_ule(bv.mk_numeral(N / 2, sz), y); - expr_ref absx = mk_ite(signx, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), x), x); - expr_ref absy = mk_ite(signy, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), y), y); + expr_ref absx = mk_ite(signx, bv.mk_bv_neg(x), x); + expr_ref absy = mk_ite(signy, bv.mk_bv_neg(y), y); expr* d = bv.mk_bv_udiv(absx, absy); sat::literal lsignx = mk_literal(signx); sat::literal lsigny = mk_literal(signy);