mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

simplify

Browse source
This commit is contained in:
Jakob Rath 2023-01-18 18:38:44 +01:00
parent 3e42dbe591
commit c62ba26cf4
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polysat/viable.cpp
View file

@ -425,7 +425,8 @@ namespace {
// a * [yil;yih] is the right-most y-interval that is completely in [lo;hi].
rational const yih = y1h + i * step;
rational const a_yih = a*yih + (k - i - 1)*M;
rational const a_yih = a_y1h + i * alpha;
SASSERT_EQ(a_yih, a*yih + (k - i - 1)*M);
SASSERT(contained(a_yih));
// The next interval to the right may contain a few more values if alpha > 0