search

OCamlPro / alt-ergo

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

feat(BV): Display BV constants using hexadecimal #1082

Closed bclement-ocp closed 5 months ago

bclement-ocp commented 5 months ago

We currently always print bit-vector constants using binary representation. This can lead to quite large values in models when using 32- or 64-bit values that are essentially unreadable. When the bit-vector width is a multiple of 4, this patch uses hexadecimal notation instead, as allowed by the SMT-LIB specification.

Note that this only applies to bit-vector terms; bit-vector semantic values are always printed in their binary representation for debugging purposes.

bclement-ocp commented 5 months ago

Looks like I forgot to update the tests for the new output syntax… derp.