mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 12:48:53 +00:00
Code Activity

enable the saturation rules

Browse source
This commit is contained in:
Jakob Rath 2024-05-10 14:59:19 +02:00
parent 7925ef731f
commit f904c08116
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/sat/smt/polysat/saturation.cpp
View file

@ -70,13 +70,13 @@ namespace polysat {
void saturation::resolve(pvar v, inequality const& i) { void saturation::resolve(pvar v, inequality const& i) {
if (c.size(v) != i.lhs().power_of_2()) if (c.size(v) != i.lhs().power_of_2())
return; return;
if (false && !c.inconsistent()) if (!c.inconsistent())
try_ugt_x(v, i); try_ugt_x(v, i);
if (false && !c.inconsistent()) if (!c.inconsistent())
try_ugt_y(v, i); try_ugt_y(v, i);
if (false && !c.inconsistent()) if (!c.inconsistent())
try_ugt_z(v, i); try_ugt_z(v, i);
if (false && !c.inconsistent()) if (!c.inconsistent())
try_eq_resolve(v, i); try_eq_resolve(v, i);
} }