Closed bclement-ocp closed 2 months ago
These are interval propagators only and respect the SMT-LIB semantics for division by 0. This requires custom operators in the Intervals module that update the bounds appropriately, sincethe existing div operator is undefined on 0.
Intervals
div
0
Note: this requires and currently includes https://github.com/OCamlPro/alt-ergo/pull/1058 and #1083 ; the commit titled "feat(BV, CP): Add propagators for bvudiv and bvurem" is new.
Rebased on #1108
bclement-ocp
commented
3 months ago
These are interval propagators only and respect the SMT-LIB semantics for division by 0. This requires custom operators in the
Intervalsmodule that update the bounds appropriately, sincethe existingdivoperator is undefined on0.Note: this requires and currently includes https://github.com/OCamlPro/alt-ergo/pull/1058 and #1083 ; the commit titled "feat(BV, CP): Add propagators for bvudiv and bvurem" is new.