OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
130 stars 33 forks source link

fix(BV, CP): Run cross-propagators to completion #1221

Closed bclement-ocp closed 2 weeks ago

bclement-ocp commented 2 weeks ago

Since #1185, when substitutions change the domain of a variable, we no longer trigger propagations, which means that we can end up in a state where the bitlist and interval domains are not consistent (i.e. running [constrain_bitlist_from_interval] or [constrain_interval_from_bitlist] would shrink some domains).

This was initially part of #1185 but was accidentally removed as part of a simplification pass during review. Add it back.

bclement-ocp commented 2 weeks ago

CI failure seems unrelated:

#=== ERROR while installing mingw-w64-shims.0.2.0 =============================#
Cannot copy D:\a\alt-ergo\alt-ergo\_opam\.opam-switch\build\mingw-w64-shims.0.2.0\shim.exe to D:\a\alt-ergo\alt-ergo\_opam\bin\x86_64-w64-mingw32-gcc.exe (C:\hostedtoolcache\windows\opam\2.2.1\x86_64\opam.exe: "open" failed on D:\a\alt-ergo\alt-ergo\_opam\bin\x86_64-w64-mingw32-gcc.exe: Permission denied).