diff --git a/bench/ce/floats.mlw b/bench/ce/floats.mlw
index 457857f30eee32b6cd11b13c5cb2c54491bda734..2fd8db5b0b0a7003ec82aa56aa0ce480f84fdef9 100644
--- a/bench/ce/floats.mlw
+++ b/bench/ce/floats.mlw
@@ -1,8 +1,33 @@
-theory T
+theory T32
 
   use import ieee_float.Float32
 
-  goal g1 : forall x:t. not (ge x (4.25:t))
+  goal g1 : forall x:t. eq x (0.0:t)
+
+  goal g2 : forall x:t. eq x (1.25:t)
+
+  goal g3 : forall x:t. not (eq x (0.0:t))
+
+  goal g4 : forall x:t. not (eq x (1.25:t))
+
+  goal g5 : forall x:t. not (ge x (4.25:t))
+
+
+end
+
+theory T64
+
+  use import ieee_float.Float64
+
+  goal g1 : forall x:t. eq x (0.0:t)
+
+  goal g2 : forall x:t. eq x (1.25:t)
+
+  goal g3 : forall x:t. not (eq x (0.0:t))
+
+  goal g4 : forall x:t. not (eq x (1.25:t))
+
+  goal g5 : forall x:t. not (ge x (4.25:t))
 
 
 end
diff --git a/bench/ce/floats_CVC4,1.5.oracle b/bench/ce/floats_CVC4,1.5.oracle
index 31a85ca81bac137be504af8a488b02e6d61159e7..d6482d9ec0e6c3a97fc5c4e56ddbf1cd6f3fd167 100644
--- a/bench/ce/floats_CVC4,1.5.oracle
+++ b/bench/ce/floats_CVC4,1.5.oracle
@@ -1,12 +1,120 @@
-bench/ce/floats.mlw T g1 : Unknown (other)
+bench/ce/floats.mlw T32 g1 : Unknown (other)
 Counter-example model:File floats.mlw:
 Line 5:
 x = {"type" : "Integer" ,
 "val" : "0" }
 
-bench/ce/floats.mlw T g1 : Unknown (other)
+bench/ce/floats.mlw T32 g2 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 7:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T32 g3 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 9:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T32 g4 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 11:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T32 g5 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 13:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T64 g1 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 22:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T64 g2 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 24:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T64 g3 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 26:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T64 g4 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 28:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T64 g5 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 30:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T32 g1 : Unknown (other)
 Counter-example model:File floats.mlw:
 Line 5:
 x = {"type" : "Integer" ,
 "val" : "0" }
 
+bench/ce/floats.mlw T32 g2 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 7:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T32 g3 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 9:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T32 g4 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 11:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T32 g5 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 13:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T64 g1 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 22:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T64 g2 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 24:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T64 g3 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 26:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T64 g4 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 28:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/floats.mlw T64 g5 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 30:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
diff --git a/bench/ce/floats_Z3,4.5.0.oracle b/bench/ce/floats_Z3,4.5.0.oracle
index 0859499882475ec2bb213e16facee87660fae717..3ba19dd39e1242758f8db87730d3306e17f23319 100644
--- a/bench/ce/floats_Z3,4.5.0.oracle
+++ b/bench/ce/floats_Z3,4.5.0.oracle
@@ -1,14 +1,128 @@
-bench/ce/floats.mlw T g1 : Unknown (other)
+bench/ce/floats.mlw T32 g1 : Unknown (other)
 Counter-example model:File floats.mlw:
 Line 5:
 x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
+"exponent" : "#x01" , "sign" : "#b1" ,
+"significand" : "#b01000000000000000000000" } }
+
+bench/ce/floats.mlw T32 g2 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 7:
+x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
+"exponent" : "#x00" , "sign" : "#b1" ,
+"significand" : "#b10000000000000000000000" } }
+
+bench/ce/floats.mlw T32 g3 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 9:
+x = {"type" : "Float" ,
+"val" : {"cons" : "Minus_zero" } }
+
+bench/ce/floats.mlw T32 g4 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 11:
+x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
+"exponent" : "#x7f" , "sign" : "#b0" ,
+"significand" : "#b01000000000000000000000" } }
+
+bench/ce/floats.mlw T32 g5 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 13:
+x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
 "exponent" : "#x81" , "sign" : "#b0" ,
 "significand" : "#b00010000000000000000000" } }
 
-bench/ce/floats.mlw T g1 : Unknown (other)
+bench/ce/floats.mlw T64 g1 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 22:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "-0x1.0000008000000p-1022" } }
+
+bench/ce/floats.mlw T64 g2 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 24:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "-0x1.0000010000000p-1023" } }
+
+bench/ce/floats.mlw T64 g3 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 26:
+x = {"type" : "Float" ,
+"val" : {"cons" : "Minus_zero" } }
+
+bench/ce/floats.mlw T64 g4 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 28:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "0x1.4000000000000p0" } }
+
+bench/ce/floats.mlw T64 g5 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 30:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "0x1.0800000000000p513" } }
+
+bench/ce/floats.mlw T32 g1 : Unknown (other)
 Counter-example model:File floats.mlw:
 Line 5:
 x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
+"exponent" : "#x01" , "sign" : "#b1" ,
+"significand" : "#b01000000000000000000000" } }
+
+bench/ce/floats.mlw T32 g2 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 7:
+x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
+"exponent" : "#x00" , "sign" : "#b1" ,
+"significand" : "#b10000000000000000000000" } }
+
+bench/ce/floats.mlw T32 g3 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 9:
+x = {"type" : "Float" ,
+"val" : {"cons" : "Minus_zero" } }
+
+bench/ce/floats.mlw T32 g4 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 11:
+x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
+"exponent" : "#x7f" , "sign" : "#b0" ,
+"significand" : "#b01000000000000000000000" } }
+
+bench/ce/floats.mlw T32 g5 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 13:
+x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
 "exponent" : "#x81" , "sign" : "#b0" ,
 "significand" : "#b00010000000000000000000" } }
 
+bench/ce/floats.mlw T64 g1 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 22:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "-0x1.0000008000000p-1022" } }
+
+bench/ce/floats.mlw T64 g2 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 24:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "-0x1.0000010000000p-1023" } }
+
+bench/ce/floats.mlw T64 g3 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 26:
+x = {"type" : "Float" ,
+"val" : {"cons" : "Minus_zero" } }
+
+bench/ce/floats.mlw T64 g4 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 28:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "0x1.4000000000000p0" } }
+
+bench/ce/floats.mlw T64 g5 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 30:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "0x1.0800000000000p513" } }
+
diff --git a/bench/ce/floats_Z3,4.6.0.oracle b/bench/ce/floats_Z3,4.6.0.oracle
index a8379e9cc09565bb3590548057a4e3b4817d8317..4f4d185edcd195727b2f84fc6d3be4b54c7eb6c5 100644
--- a/bench/ce/floats_Z3,4.6.0.oracle
+++ b/bench/ce/floats_Z3,4.6.0.oracle
@@ -1,14 +1,128 @@
-bench/ce/floats.mlw T g1 : Unknown (other)
+bench/ce/floats.mlw T32 g1 : Unknown (other)
 Counter-example model:File floats.mlw:
 Line 5:
 x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
+"exponent" : "#x01" , "sign" : "#b1" ,
+"significand" : "#b00100000000000000000000" } }
+
+bench/ce/floats.mlw T32 g2 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 7:
+x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
+"exponent" : "#x00" , "sign" : "#b1" ,
+"significand" : "#b00000000000000000000001" } }
+
+bench/ce/floats.mlw T32 g3 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 9:
+x = {"type" : "Float" ,
+"val" : {"cons" : "Minus_zero" } }
+
+bench/ce/floats.mlw T32 g4 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 11:
+x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
+"exponent" : "#x7f" , "sign" : "#b0" ,
+"significand" : "#b01000000000000000000000" } }
+
+bench/ce/floats.mlw T32 g5 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 13:
+x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
 "exponent" : "#xc0" , "sign" : "#b0" ,
 "significand" : "#b00000000000000000000001" } }
 
-bench/ce/floats.mlw T g1 : Unknown (other)
+bench/ce/floats.mlw T64 g1 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 22:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "-0x1.0100000000000p-1022" } }
+
+bench/ce/floats.mlw T64 g2 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 24:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "-0x1.0000000000400p-1023" } }
+
+bench/ce/floats.mlw T64 g3 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 26:
+x = {"type" : "Float" ,
+"val" : {"cons" : "Minus_zero" } }
+
+bench/ce/floats.mlw T64 g4 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 28:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "0x1.4000000000000p0" } }
+
+bench/ce/floats.mlw T64 g5 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 30:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "0x1.0000000000001p513" } }
+
+bench/ce/floats.mlw T32 g1 : Unknown (other)
 Counter-example model:File floats.mlw:
 Line 5:
 x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
+"exponent" : "#x01" , "sign" : "#b1" ,
+"significand" : "#b00100000000000000000000" } }
+
+bench/ce/floats.mlw T32 g2 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 7:
+x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
+"exponent" : "#x00" , "sign" : "#b1" ,
+"significand" : "#b00000000000000000000001" } }
+
+bench/ce/floats.mlw T32 g3 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 9:
+x = {"type" : "Float" ,
+"val" : {"cons" : "Minus_zero" } }
+
+bench/ce/floats.mlw T32 g4 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 11:
+x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
+"exponent" : "#x7f" , "sign" : "#b0" ,
+"significand" : "#b01000000000000000000000" } }
+
+bench/ce/floats.mlw T32 g5 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 13:
+x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
 "exponent" : "#xc0" , "sign" : "#b0" ,
 "significand" : "#b00000000000000000000001" } }
 
+bench/ce/floats.mlw T64 g1 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 22:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "-0x1.0100000000000p-1022" } }
+
+bench/ce/floats.mlw T64 g2 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 24:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "-0x1.0000000000400p-1023" } }
+
+bench/ce/floats.mlw T64 g3 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 26:
+x = {"type" : "Float" ,
+"val" : {"cons" : "Minus_zero" } }
+
+bench/ce/floats.mlw T64 g4 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 28:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "0x1.4000000000000p0" } }
+
+bench/ce/floats.mlw T64 g5 : Unknown (other)
+Counter-example model:File floats.mlw:
+Line 30:
+x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
+"value" : "0x1.0000000000001p513" } }
+
diff --git a/src/core/model_parser.ml b/src/core/model_parser.ml
index 7ea9435a20067ec0af4a5c27d4e370a4b89bc53c..de89d705ef31d36c0980b9c586fee4afa7bff438 100644
--- a/src/core/model_parser.ml
+++ b/src/core/model_parser.ml
@@ -34,6 +34,7 @@ type float_type =
   | Minus_zero
   | Not_a_number
   | Float_value of string * string * string
+  | Float_hexa of string
 
 type model_value =
  | Integer of string
@@ -99,6 +100,10 @@ let convert_float_value f =
       let m = Mstr.add "exponent" (Json_base.String eb) m in
       let m = Mstr.add "significand" (Json_base.String sb) m in
       Json_base.Record m
+  | Float_hexa s ->
+      let m = Mstr.add "cons" (Json_base.String "Float_hexa") Stdlib.Mstr.empty in
+      let m = Mstr.add "value" (Json_base.String s) m in
+      Json_base.Record m
 
 let rec convert_model_value value : Json_base.json =
   match value with
@@ -200,7 +205,8 @@ let print_float_human fmt f =
   | Not_a_number ->
       fprintf fmt "NaN"
   | Float_value (b, eb, sb) ->
-      fprintf fmt "float(%s,%s,%s)" b eb sb
+     fprintf fmt "float_bits(%s,%s,%s)" b eb sb
+  | Float_hexa s -> fprintf fmt "%s" s
 
 let rec print_array_human fmt (arr: model_array) =
   fprintf fmt "(";
diff --git a/src/core/model_parser.mli b/src/core/model_parser.mli
index e921949caca0f3aa1c9282299c1ab39d8f498313..0f61dd961a55b48695100a05282e436a57fff8cc 100644
--- a/src/core/model_parser.mli
+++ b/src/core/model_parser.mli
@@ -22,6 +22,7 @@ type float_type =
   | Minus_zero
   | Not_a_number
   | Float_value of string * string * string
+  | Float_hexa of string
 
 type model_value =
  | Integer of string
diff --git a/src/driver/collect_data_model.ml b/src/driver/collect_data_model.ml
index 731df62d0fc4a7da87cd64fbd8fc125a173ebdcc..e02a5358d7348b1233bd66c274782758db806853 100644
--- a/src/driver/collect_data_model.ml
+++ b/src/driver/collect_data_model.ml
@@ -211,15 +211,6 @@ and refine_variable_value (table: correspondence_table) key v =
     let tv = refine_definition table t in
     Mstr.add key (true, tv) table
 
-let convert_float (f: Smt2_model_defs.float_type) : Model_parser.float_type =
-  match f with
-  | Plus_infinity           -> Model_parser.Plus_infinity
-  | Minus_infinity          -> Model_parser.Minus_infinity
-  | Plus_zero               -> Model_parser.Plus_zero
-  | Minus_zero              -> Model_parser.Minus_zero
-  | Not_a_number            -> Model_parser.Not_a_number
-  | Float_value (b, eb, sb) -> Model_parser.Float_value (b, eb, sb)
-
 (* Conversion to value referenced as defined in model_parser.
    We assume that array indices fit into an integer *)
 let convert_to_indice t =
@@ -249,7 +240,7 @@ and convert_to_model_value (t: term): Model_parser.model_value =
   | Integer i -> Model_parser.Integer i
   | Decimal (d1, d2) -> Model_parser.Decimal (d1, d2)
   | Fraction (s1, s2) -> Model_parser.Fraction (s1, s2)
-  | Float f -> Model_parser.Float (convert_float f)
+  | Float f -> Model_parser.Float f
   | Bitvector bv -> Model_parser.Bitvector bv
   | Boolean b -> Model_parser.Boolean b
   | Other _s -> raise Not_value
diff --git a/src/driver/parse_smtv2_model_lexer.mll b/src/driver/parse_smtv2_model_lexer.mll
index 7c6523c0ef97b1602d7595d89816060826cb97fa..77f05f6ff85aeb114d10c9f76a89c15967d54bc1 100644
--- a/src/driver/parse_smtv2_model_lexer.mll
+++ b/src/driver/parse_smtv2_model_lexer.mll
@@ -12,6 +12,31 @@
 {
   open Parse_smtv2_model_parser
   exception SyntaxError
+
+  let interp_float b eb sb =
+    try
+      let is_neg = match b with
+        | "#b0" -> false
+        | "#b1" -> true
+        | _ -> raise Exit
+      in
+      if String.sub eb 0 2 = "#b" && String.length eb = 13 &&
+         String.sub sb 0 2 = "#x" && String.length sb = 15 then
+         (* binary 64 *)
+         let exp_base2 = String.sub eb 2 11 in
+         let exp = int_of_string ("0b" ^ exp_base2) - 1023 in
+         let mant_base16 = String.sub sb 2 13 in
+         Model_parser.Float_hexa((if is_neg then "-" else "")^
+         "0x1."^mant_base16^"p"^(string_of_int exp))
+      else
+      if String.sub eb 0 2 = "#x" && String.length eb = 4 &&
+         String.sub sb 0 2 = "#b" && String.length eb = 25 then
+         (* binary 32 *)
+         let exp_base16 = String.sub eb 2 2 in
+         let mant_base2 = String.sub sb 2 23 in
+           raise Exit (* TODO *)
+         else raise Exit
+   with Exit -> Model_parser.Float_value (b, eb, sb)
 }
 
 let atom = [^'('')'' ''\t''\n']
@@ -63,13 +88,13 @@ rule token = parse
   | "(_" space+ "BitVec" space+ num")" { BITVECTOR_TYPE }
   | "(_" space+ "extract" space+ num space+ num ")" as s { BITVECTOR_EXTRACT s }
 
-  | "(_" space+ "+zero" space+ num space+ num ")" { FLOAT_VALUE Smt2_model_defs.Plus_zero }
-  | "(_" space+ "-zero" space+ num space+ num ")" { FLOAT_VALUE Smt2_model_defs.Minus_zero }
-  | "(_"  space+ "+oo" space+ num space+ num ")" { FLOAT_VALUE Smt2_model_defs.Plus_infinity }
-  | "(_" space+ "-oo" space+ num space+ num ")" { FLOAT_VALUE Smt2_model_defs.Minus_infinity }
-  | "(_" space+ "NaN" space+ num space+ num ")" { FLOAT_VALUE Smt2_model_defs.Not_a_number }
+  | "(_" space+ "+zero" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Plus_zero }
+  | "(_" space+ "-zero" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Minus_zero }
+  | "(_"  space+ "+oo" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Plus_infinity }
+  | "(_" space+ "-oo" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Minus_infinity }
+  | "(_" space+ "NaN" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Not_a_number }
   | "(fp" space+ (float_num as b) space+ (float_num as eb) space+ (float_num as sb) ")"
-      { FLOAT_VALUE (Smt2_model_defs.Float_value (b, eb, sb)) }
+      { FLOAT_VALUE (interp_float b eb sb) }
 
   | num as integer
       { INT_STR (integer) }
diff --git a/src/driver/parse_smtv2_model_parser.mly b/src/driver/parse_smtv2_model_parser.mly
index 220926861de71ff5397e7de78cf61b2c80905d68..0673706b9afac6e55e791fb752ed16dcbbb74bf9 100644
--- a/src/driver/parse_smtv2_model_parser.mly
+++ b/src/driver/parse_smtv2_model_parser.mly
@@ -33,7 +33,7 @@
 %token LET
 %token AND LE GE NOT
 %token DIV
-%token <Smt2_model_defs.float_type> FLOAT_VALUE
+%token <Model_parser.float_type> FLOAT_VALUE
 %token <string> COMMENT
 %token <string> BITVECTOR_VALUE
 %token <string> BITVECTOR_EXTRACT
diff --git a/src/driver/smt2_model_defs.ml b/src/driver/smt2_model_defs.ml
index 0c8d5156eeddcc47a1b05b910da68dfa5872f582..489e8d57de9d2ff1221ef1b7813d1ee36e180a95 100644
--- a/src/driver/smt2_model_defs.ml
+++ b/src/driver/smt2_model_defs.ml
@@ -13,14 +13,6 @@ open Stdlib
 
 type variable = string
 
-type float_type =
-  | Plus_infinity
-  | Minus_infinity
-  | Plus_zero
-  | Minus_zero
-  | Not_a_number
-  | Float_value of string * string * string
-
 type array =
   | Const of term
   | Store of array * term * term
@@ -29,7 +21,7 @@ and term =
   | Integer of string
   | Decimal of (string * string)
   | Fraction of (string * string)
-  | Float of float_type
+  | Float of Model_parser.float_type
   | Apply of (string * term list)
   | Other of string
   | Array of array
@@ -54,12 +46,13 @@ type correspondence_table = (bool * definition) Mstr.t
 
 let print_float fmt f =
   match f with
-  | Plus_infinity -> Format.fprintf fmt "Plus_infinity"
-  | Minus_infinity -> Format.fprintf fmt "Minus_infinity"
-  | Plus_zero -> Format.fprintf fmt "Plus_zero"
-  | Minus_zero -> Format.fprintf fmt "Minus_zero"
-  | Not_a_number -> Format.fprintf fmt "NaN"
-  | Float_value (b, eb, sb) -> Format.fprintf fmt "(%s, %s, %s)" b eb sb
+  | Model_parser.Plus_infinity -> Format.fprintf fmt "Plus_infinity"
+  | Model_parser.Minus_infinity -> Format.fprintf fmt "Minus_infinity"
+  | Model_parser.Plus_zero -> Format.fprintf fmt "Plus_zero"
+  | Model_parser.Minus_zero -> Format.fprintf fmt "Minus_zero"
+  | Model_parser.Not_a_number -> Format.fprintf fmt "NaN"
+  | Model_parser.Float_value (b, eb, sb) -> Format.fprintf fmt "(%s, %s, %s)" b eb sb
+  | Model_parser.Float_hexa s -> Format.fprintf fmt "%s" s
 
 let rec print_array fmt a =
   match a with
diff --git a/src/driver/smt2_model_defs.mli b/src/driver/smt2_model_defs.mli
index 7e327c7409bee2d11a7b7920639093632911238f..eddab91b20ab69fafef4ae9a29bb63ece4d97da2 100644
--- a/src/driver/smt2_model_defs.mli
+++ b/src/driver/smt2_model_defs.mli
@@ -13,14 +13,6 @@ open Stdlib
 
 type variable = string
 
-type float_type =
-  | Plus_infinity
-  | Minus_infinity
-  | Plus_zero
-  | Minus_zero
-  | Not_a_number
-  | Float_value of string * string * string
-
 type array =
   | Const of term
   | Store of array * term * term
@@ -29,7 +21,7 @@ and term =
   | Integer of string
   | Decimal of (string * string)
   | Fraction of (string * string)
-  | Float of float_type
+  | Float of Model_parser.float_type
   | Apply of (string * term list)
   | Other of string
   | Array of array