Bump colibri2 pin

formalsec · Feb 18, 2025 · 34f6e9f · 34f6e9f
1 parent 9b08df5
commit 34f6e9f
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 12 deletions.
diff --git 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
@@ -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
@@ -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