From 7a96853721bf3821b40d3ca0c07a0407b597bdfc Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 27 Jul 2023 15:34:58 +0200 Subject: [PATCH] fix --- src/math/polysat/constraint_manager.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp index 371b252aa..f29bfa16b 100644 --- a/src/math/polysat/constraint_manager.cpp +++ b/src/math/polysat/constraint_manager.cpp @@ -659,7 +659,7 @@ namespace polysat { unsigned const p_sz = p.power_of_2(); unsigned const v_sz = p_sz + extra_bits; if (p.is_val()) - return s.sz2pdd(v_sz).mk_val(p.val_signed()); + return s.sz2pdd(v_sz).mk_val(p.get_signed_val()); pdd const q = s.var(s.m_names.mk_name(p)); constraint_dedup::bv_ext_args const args = {true, q.var(), extra_bits}; auto const it = m_dedup.m_bv_ext_expr.find_iterator(args);