mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

bug with sizes

Browse source
This commit is contained in:
Jakob Rath 2024-02-08 14:20:26 +01:00
parent 0cef6bec4e
commit 0ada7f8e40
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/smt/polysat/viable.cpp
View file

@ -702,9 +702,10 @@ namespace polysat {
unsigned const w_sz = c.size(w);
unsigned const z_sz = offset;
unsigned const y_sz = std::min(w_sz, v_sz - z_sz);
unsigned const x_sz = v_sz - y_sz;
unsigned const x_sz = v_sz - y_sz - z_sz;
rational const& w_shift = rational::power_of_two(w_sz - y_sz);
verbose_stream() << "v_sz " << v_sz << " w_sz " << w_sz << " / x_sz " << x_sz << " y_sz " << y_sz << " z_sz " << z_sz << "\n";
SASSERT_EQ(v_sz, x_sz + y_sz + z_sz);
SASSERT(!e->interval.is_full());
rational const& lo = e->interval.lo_val();