feat(BV): Display BV constants using hexadecimal

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.

src/lib/structures/expr.ml

@@ -462,7 +462,10 @@ module SmtPrinter = struct
       pp_rational ppf q
 
     | Sy.Bitv (n, s), [] ->
-      Fmt.pf ppf "#b%s" (Z.format (Fmt.str "%%0%db" n) s)
+      if n mod 4 = 0 then
+        Fmt.pf ppf "#x%s" (Z.format (Fmt.str "%%0%dx" (n / 4)) s)
+      else
+        Fmt.pf ppf "#b%s" (Z.format (Fmt.str "%%0%db" n) s)
 
     | Sy.MapsTo v, [t] ->
       Fmt.pf ppf "@[<2>(ae.mapsto %a %a@])" Var.print v pp t