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

need y0 value

Browse source
This commit is contained in:
Jakob Rath 2023-01-05 16:43:23 +01:00
parent ffa12eb37c
commit 6f18335604
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/saturation.cpp
View file

@ -1700,6 +1700,8 @@ namespace polysat {
if (y1 == null_var && y2 == null_var)
return false;
y = (y1 == null_var) ? y2 : y1;
if (!s.is_assigned(y))
return false;
rational y0 = s.get_value(y);
vector<signed_constraint> bounds;