mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

update

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-27 20:20:51 -08:00
parent 67b9ecbd97
commit b52379fe88
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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)