From f904c08116bf2aeb12ee2dfcb78b880321edd1e0 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 10 May 2024 14:59:19 +0200 Subject: [PATCH] enable the saturation rules --- src/sat/smt/polysat/saturation.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/sat/smt/polysat/saturation.cpp b/src/sat/smt/polysat/saturation.cpp index 6b28c5e60..8a21c873b 100644 --- a/src/sat/smt/polysat/saturation.cpp +++ b/src/sat/smt/polysat/saturation.cpp @@ -70,13 +70,13 @@ namespace polysat { void saturation::resolve(pvar v, inequality const& i) { if (c.size(v) != i.lhs().power_of_2()) return; - if (false && !c.inconsistent()) + if (!c.inconsistent()) try_ugt_x(v, i); - if (false && !c.inconsistent()) + if (!c.inconsistent()) try_ugt_y(v, i); - if (false && !c.inconsistent()) + if (!c.inconsistent()) try_ugt_z(v, i); - if (false && !c.inconsistent()) + if (!c.inconsistent()) try_eq_resolve(v, i); }