Skip to content

Fix slowdown in bv_saturate from https://github.com/coq/coq/pull/17984

Michael Sammler requested to merge msammler/euclidean_division_cleanup_slowdown into master

https://github.com/coq/coq/pull/17984 causes a significant slowdown in Islaris since the changed Z.euclidean_division_equations_cleanup function can be become very slow if there are many hypothesis of the form 0 <= ... < ... in the context. This MR works around this by changing bv_saturate to generate hypothesis of the form -1 < ... < ... instead of 0 <= ... < .... This change speeds up some case studies in Islaris by up to 30%, see here.

Merge request reports