Bitvector `bv%i` is broken about dolmen HOT 7 CLOSED

I thought about it when writing it but from what I understand there will be problems only if a problem make use of bitvectors whose size is strictly greater than 2 ^ 62, (in which case, I don't think parsing such a bitvector litteral will be realistic, so only symbolic manipulation may be done, but I guess this can happen ?), or am I missing something ?

from dolmen.

No, just a bitvector of size 62, it is the actual value of the bitvector that goes through int_of_string not just the size.

from dolmen.

(define-fun big () (_ BitVec 334) (_ bv9999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999 334))

from dolmen.

Oh, indeed that's a problem. We'll have to write a manual conversion to strings in that case (I'd rather avoid depending on zarith for now if not absolutely necessary).

from dolmen.

So https://stackoverflow.com/a/11007021/1531323 for direct conversion to binary ?

from dolmen.

For reference the code with zarith (for COLIBRI I fixed it that way temporarily):

    let parse_extended_lit _env _ast s n =
      assert (String.length s >= 2);
      let s' = String.sub s 2 (String.length s - 2) in
      match Z.of_string s' with
      | exception Failure _ -> None
      | z ->
        let z = Z.rem z (Z.shift_left Z.one n) in
        let s'' = Z.format (Printf.sprintf "%%0%ib" n) z in
        Some (Type.Term (T.mk_bitv s''))

from dolmen.

So https://stackoverflow.com/a/11007021/1531323 for direct conversion to binary ?

Yes, i'll try and implement it as soon as possible.

from dolmen.