mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

We shouldn't assume that v is assigned

Browse source 
Happens if it is a viable conflict for v
This commit is contained in:
Jakob Rath 2022-12-08 15:52:34 +01:00
parent 3fe8f4a0cd
commit a81e05e660
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -346,7 +346,7 @@ namespace polysat {
if (!is_xY_l_xZ(v, xy_l_xz, y, z))
return false;
if (!xy_l_xz.is_strict() && s.get_value(v).is_zero())
if (!xy_l_xz.is_strict() && s.is_assigned(v) && s.get_value(v).is_zero())
return false;
if (!is_non_overflow(x, y, non_ovfl))
return false;