From b52379fe883833b96a4cd723a6ec33a7da0ee9f5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 Dec 2022 20:20:51 -0800 Subject: [PATCH] update Signed-off-by: Nikolaj Bjorner --- src/math/polysat/saturation.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 9e6f0ec60..00c1c1d5b 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -1355,12 +1355,12 @@ namespace polysat { * = max y . r(x_max,y) < N, where x_max = 2^128-1 * = max y . y*x_max - 1 <= N - 1 * = floor(N / x_max) - * = 2^128 + * = 2^128 + 1 * * max y . q(x, y) < N * = max y . (y + 1) * x_max - 1 <= N -1 * = floor(N / x_max) - 1 - * = 2^128 - 1 (NSB: this is a weaker bound than what it should be. Is using "floor" too much?) + * = 2^128 * * min y . 0 < r(x,y) forall x in A_x * = min y . 0 < r(x_min, y)