From c894efd777ee574f36c4b8684a40a4629108b183 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Sep 2021 14:06:46 +0200 Subject: [PATCH] nit Signed-off-by: Nikolaj Bjorner --- src/math/polysat/saturation.cpp | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index f5c41c2eb..b50f9e685 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -231,15 +231,9 @@ namespace polysat { // (extension to arbitrary monomials for 'x' should be fairly easy too) if (!x.is_unary()) return false; - unsigned x_var = x.var(); rational x_coeff = x.hi().val(); pdd xz = x; - if (!c.rhs.try_div(x_coeff, xz)) - return false; - if (!xz.factor(x_var, 1, z)) - return false; - LOG("zx > yx: " << show_deref(c.src)); - return true; + return c.rhs.try_div(x_coeff, xz) && xz.factor(x.var(), 1, z); } bool inf_saturate::verify_Xy_l_XZ(pvar v, inequality const& c, pdd const& x, pdd const& z) {