diff --git a/smtml.opam b/smtml.opam index 3d0c1fad..4103bf49 100644 --- a/smtml.opam +++ b/smtml.opam @@ -71,8 +71,8 @@ build: [ dev-repo: "git+https://github.com/formalsec/smtml.git" available: arch != "arm32" & arch != "x86_32" pin-depends: [ - ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#1feba887bbb7980f27bbcec8137eb908caa8f0ce"] - ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#1feba887bbb7980f27bbcec8137eb908caa8f0ce"] + ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#e15e6fc52b1f4e9a015b630a1f377d203ed9ec5b"] + ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#e15e6fc52b1f4e9a015b630a1f377d203ed9ec5b"] ["alt-ergo-lib.2.6.0" "git+https://github.com/OCamlPro/alt-ergo.git#7ee96296a5de9588a4d585b3b8abec35f4755425"] ["cvc5.dev" "git+https://github.com/formalsec/ocaml-cvc5.git#b7aade52d49a19d646036d7e6aac09039c3e95cf"] ["benchpress.dev" "git+https://github.com/sneeuwballen/benchpress.git#7f44cdd9f0511afcce2c9ad3c04cc9b72919bcff"] diff --git a/smtml.opam.template b/smtml.opam.template index c539b812..ecf6b54d 100644 --- a/smtml.opam.template +++ b/smtml.opam.template @@ -1,7 +1,7 @@ available: arch != "arm32" & arch != "x86_32" pin-depends: [ - ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#1feba887bbb7980f27bbcec8137eb908caa8f0ce"] - ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#1feba887bbb7980f27bbcec8137eb908caa8f0ce"] + ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#e15e6fc52b1f4e9a015b630a1f377d203ed9ec5b"] + ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#e15e6fc52b1f4e9a015b630a1f377d203ed9ec5b"] ["alt-ergo-lib.2.6.0" "git+https://github.com/OCamlPro/alt-ergo.git#7ee96296a5de9588a4d585b3b8abec35f4755425"] ["cvc5.dev" "git+https://github.com/formalsec/ocaml-cvc5.git#b7aade52d49a19d646036d7e6aac09039c3e95cf"] ["benchpress.dev" "git+https://github.com/sneeuwballen/benchpress.git#7f44cdd9f0511afcce2c9ad3c04cc9b72919bcff"] diff --git a/src/smtml/colibri2_mappings.default.ml b/src/smtml/colibri2_mappings.default.ml index eb339b7d..d458ca15 100644 --- a/src/smtml/colibri2_mappings.default.ml +++ b/src/smtml/colibri2_mappings.default.ml @@ -274,20 +274,16 @@ module Fresh = struct with | Some a when A.is_integer a -> Some (Value.Int (A.to_int a)) | Some a when A.is_real a -> - Some (Value.Real (Float.of_string (A.to_string a))) + Option.map + (fun f -> Value.Real f) + (Float.of_string_opt (A.to_string a)) | Some _ | None -> None ) | Ty_bitv n -> ( match Colibri2_core.Value.value Colibri2_theories_LRA.RealValue.key v with | Some a when A.is_integer a -> - Some - (Value.Num - ( match n with - | 8 -> I8 (A.to_int a) - | 32 -> I32 (Int32.of_int (A.to_int a)) - | 64 -> I64 (Int64.of_int (A.to_int a)) - | _ -> assert false ) ) + Some (Value.Bitv (Bitvector.make (A.to_z a) n)) | _ -> assert false ) | Ty_fp n -> ( match Colibri2_core.Value.value Colibri2_theories_fp.Fp_value.key v with