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

enable

Browse source
This commit is contained in:
Jakob Rath 2022-12-07 18:45:00 +01:00
parent 45e94ae7dd
commit 55d691e16e
1 changed files with 0 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -39,14 +39,10 @@ namespace polysat {
if (c.is_currently_true(s))
continue;
auto i = inequality::from_ule(c);
#if 0
if (try_mul_bounds(v, core, i))
return true;
#endif
#if 0
if (try_parity(v, core, i))
return true;
#endif
if (try_ugt_x(v, core, i))
return true;
if (try_ugt_y(v, core, i))