search

OCamlPro / alt-ergo

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

fix(BV): Properly set fully interpreted operators #1073

Closed bclement-ocp closed 5 months ago

bclement-ocp commented 5 months ago

Alt-Ergo calls "fully interpreted" symbols that are fully internalized in semantic values and do not need to be taken into consideration by the CC(X) algorithm (see function congruents in ccx.ml).

(Note that fully_interpreted is only called for the Shostak theory associated with the symbol according to is_min_symb.)

The BV theory incorrectly states that all its symbols are fully interpreted, including bv2nat, int2bv, etc.; however, only concat, extract and bv2nat are fully interpreted. This means that Alt-Ergo never performs congruence closure for these functions, leading to missed reasoning opportunities.

bclement-ocp commented 5 months ago

(CI failures are unrelated and should be fixed by #1074)