diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 95ab99490..fe102414d 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -178,6 +178,8 @@ end
 (** Builtins *)
 type _ DStd.Builtin.t +=
   | Float
+  | AERound of int * int
+  (** Equivalent of Float for the SMT2 format. *)
   | Integer_round
   | Abs_real
   | Sqrt_real
@@ -193,6 +195,49 @@ type _ DStd.Builtin.t +=
   (* Internal use for semantic triggers -- do not expose outside of theories *)
   | Not_theory_constant | Is_theory_constant | Linear_dependency
 
+let builtin_term t = Dl.Typer.T.builtin_term t
+
+let builtin_ty t = Dl.Typer.T.builtin_ty t
+
+let ty name ty =
+  Id.Map.add { name = DStd.Name.simple name; ns = Sort } @@
+  fun env s ->
+  builtin_ty @@
+  Dolmen_type.Base.app0 (module Dl.Typer.T) env s ty
+
+let builtin_enum = function
+  | Ty.Tsum (name, cstrs) as ty_ ->
+    let ty_cst =
+      DStd.Expr.Id.mk ~builtin:B.Base
+        (DStd.Path.global (Hstring.view name))
+        DStd.Expr.{ arity = 0; alias = No_alias }
+    in
+    let cstrs =
+      List.map (fun c -> DStd.Path.global (Hstring.view c), []) cstrs
+    in
+    let _, cstrs = DStd.Expr.Term.define_adt ty_cst [] cstrs in
+    let dty = DT.apply ty_cst [] in
+    let add_cstrs map =
+      List.fold_left (fun map ((c : DE.term_cst), _) ->
+          let name = get_basename c.path in
+          Id.Map.add { name = DStd.Name.simple name; ns = Term } (fun env _ ->
+              builtin_term @@
+              Dolmen_type.Base.term_app_cst
+                (module Dl.Typer.T) env c) map)
+        map cstrs
+    in
+    Cache.store_ty (DE.Ty.Const.hash ty_cst) ty_;
+    dty,
+    cstrs,
+    fun map ->
+      map
+      |> ty (Hstring.view name) dty
+      |> add_cstrs
+  | _ -> assert false
+
+let fpa_rounding_mode, rounding_modes, add_rounding_modes =
+  builtin_enum Fpa_rounding.fpa_rounding_mode
+
 module Const = struct
   open DE
 
@@ -207,6 +252,15 @@ module Const = struct
         let name = "int2bv" in
         Id.mk ~name ~builtin:(Int2BV n)
           (DStd.Path.global name) Ty.(arrow [int] (bitv n)))
+
+  let smt_round =
+    with_cache (fun (n, m) ->
+        let name = "ae.round" in
+        Id.mk
+          ~name
+          ~builtin:(AERound (n, m))
+          (DStd.Path.global name)
+          Ty.(arrow [fpa_rounding_mode; real] real))
 end
 
 let bv2nat t =
@@ -220,6 +274,9 @@ let bv2nat t =
 let int2bv n t =
   DE.Term.apply_cst (Const.int2bv n) [] [t]
 
+let smt_round n m rm t =
+  DE.Term.apply_cst (Const.smt_round (n, m)) [] [rm; t]
+
 let bv_builtins env s =
   let term_app1 f =
     Dl.Typer.T.builtin_term @@
@@ -241,54 +298,49 @@ let bv_builtins env s =
     end
   | _ -> `Not_found
 
-let fpa_builtins =
+(** Takes a dolmen identifier [id] and injects it in Alt-Ergo's registered
+    identifiers.
+    It transforms "fpa_rounding_mode", the Alt-Ergo builtin type into the SMT2
+    rounding type "RoundingMode". Also injects each constructor into their SMT2
+    equivalent *)
+let inject_ae_to_smt2 id =
+  match id with
+  | Id.{name = Simple n; _} ->
+    begin
+      if String.equal n Fpa_rounding.fpa_rounding_mode_ae_type_name then
+        (* Injecting the type name as the SMT2 Type name. *)
+        let name =
+          Dolmen_std.Name.simple Fpa_rounding.fpa_rounding_mode_type_name
+        in
+        {id with name}
+      else
+        match Fpa_rounding.rounding_mode_of_ae_hs (Hstring.make n) with
+        | rm ->
+          let name =
+            Dolmen_std.Name.simple (Fpa_rounding.string_of_rounding_mode rm)
+          in
+          {id with name}
+        | exception (Failure _) ->
+          id
+    end
+  | id -> id
+
+let ae_fpa_builtins =
   let (->.) args ret = (args, ret) in
-  let builtin_term t = Dl.Typer.T.builtin_term t in
-  let builtin_ty t = Dl.Typer.T.builtin_ty t in
   let dterm name f =
     Id.Map.add { name = DStd.Name.simple name; ns = Term } @@
     fun env s ->
     builtin_term @@
     Dolmen_type.Base.term_app1 (module Dl.Typer.T) env s f
   in
-  let ty name ty =
-    Id.Map.add { name = DStd.Name.simple name; ns = Sort } @@
-    fun env s ->
-    builtin_ty @@
-    Dolmen_type.Base.app0 (module Dl.Typer.T) env s ty
-  in
-  let builtin_enum = function
-    | Ty.Tsum (name, cstrs) as ty_ ->
-      let ty_cst =
-        DStd.Expr.Id.mk ~builtin:B.Base
-          (DStd.Path.global (Hstring.view name))
-          DStd.Expr.{ arity = 0; alias = No_alias }
-      in
-      let cstrs =
-        List.map (fun c -> DStd.Path.global (Hstring.view c), []) cstrs
-      in
-      let _, cstrs = DStd.Expr.Term.define_adt ty_cst [] cstrs in
-      let dty = DT.apply ty_cst [] in
-      let add_cstrs map =
-        List.fold_left (fun map ((c : DE.term_cst), _) ->
-            let name = get_basename c.path in
-            Id.Map.add { name = DStd.Name.simple name; ns = Term } (fun env _ ->
-                builtin_term @@
-                Dolmen_type.Base.term_app_cst
-                  (module Dl.Typer.T) env c) map)
-          map cstrs
-      in
-      Cache.store_ty (DE.Ty.Const.hash ty_cst) ty_;
-      dty,
-      cstrs,
-      fun map ->
-        map
-        |> ty (Hstring.view name) dty
-        |> add_cstrs
-    | _ -> assert false
-  in
-  let fpa_rounding_mode, rounding_modes, add_rounding_modes =
-    builtin_enum Fpa_rounding.fpa_rounding_mode
+  let op ?(tyvars = []) name builtin (args, ret) =
+    let ty = DT.pi tyvars @@ DT.arrow args ret in
+    let cst = DE.Id.mk ~name ~builtin (DStd.Path.global name) ty in
+    Id.Map.add { name = DStd.Name.simple name; ns = Term } @@
+    fun env _ ->
+    builtin_term @@
+    Dolmen_type.Base.term_app_cst
+      (module Dl.Typer.T) env cst
   in
   let float_cst =
     let ty = DT.(arrow [int; int; fpa_rounding_mode; real] real) in
@@ -311,15 +363,6 @@ let fpa_builtins =
   let float32d x = float32 (mode "NearestTiesToEven") x in
   let float64 = float (DE.Term.int "53") (DE.Term.int "1074") in
   let float64d x = float64 (mode "NearestTiesToEven") x in
-  let op ?(tyvars = []) name builtin (args, ret) =
-    let ty = DT.pi tyvars @@ DT.arrow args ret in
-    let cst = DE.Id.mk ~name ~builtin (DStd.Path.global name) ty in
-    Id.Map.add { name = DStd.Name.simple name; ns = Term } @@
-    fun env _ ->
-    builtin_term @@
-    Dolmen_type.Base.term_app_cst
-      (module Dl.Typer.T) env cst
-  in
   let partial1 name f =
     Id.Map.add { name = DStd.Name.simple name; ns = Term } @@
     fun env s ->
@@ -335,7 +378,11 @@ let fpa_builtins =
   let is_theory_constant =
     let open DT in
     let a = Var.mk "alpha" in
-    op ~tyvars:[a] "is_theory_constant" Is_theory_constant ([of_var a] ->. prop)
+    op
+      ~tyvars:[a]
+      "is_theory_constant"
+      Is_theory_constant
+      ([of_var a] ->. prop)
   in
   let fpa_builtins =
     let open DT in
@@ -409,24 +456,61 @@ let fpa_builtins =
     |> op "not_theory_constant" Not_theory_constant ([real] ->. prop)
     |> is_theory_constant
     |> op "linear_dependency" Linear_dependency ([real; real] ->. prop)
-
   in
   fun env s ->
-    begin match s with
-      | Dl.Typer.T.Id id ->
-        begin
-          try
-            Id.Map.find_exn id fpa_builtins env s
-          with Not_found -> `Not_found
-        end
-      | Builtin _ -> `Not_found
-    end
+    let search_id id =
+      try
+        Id.Map.find_exn id fpa_builtins env s
+      with Not_found -> `Not_found
+    in
+    match s with
+    | Dl.Typer.T.Id id ->
+      let new_id = inject_ae_to_smt2 id in
+      search_id new_id
+    | Builtin _ -> `Not_found
+
+let smt_fpa_builtins =
+  let term_app env s f =
+    Dl.Typer.T.builtin_term @@
+    Dolmen_type.Base.term_app2 (module Dl.Typer.T) env s f
+  in
+  let other_builtins =
+    Id.Map.empty
+    |> add_rounding_modes
+  in
+  fun env s ->
+    match s with
+    | Dl.Typer.T.Id {
+        ns = Term ;
+        name = Indexed {
+            basename = "ae.round" ;
+            indexes = [ i; j ] } } ->
+      begin match
+          int_of_string i,
+          int_of_string j
+        with
+        | n, m -> term_app env s (smt_round n m)
+        | exception Failure _ -> `Not_found
+      end
+    | Dl.Typer.T.Id id -> begin
+        match Id.Map.find_exn id other_builtins env s with
+        | e -> e
+        | exception Not_found -> `Not_found
+      end
+    | _ -> `Not_found
+
+(** Concatenation of builtins handlers. *)
+let (++) bt1 bt2 =
+  fun a b ->
+  match bt1 a b with
+  | `Not_found -> bt2 a b
+  | res -> res
 
 let builtins =
   fun _st (lang : Typer.lang) ->
   match lang with
-  | `Logic Alt_ergo -> fpa_builtins
-  | `Logic (Smtlib2 _) -> bv_builtins
+  | `Logic Alt_ergo -> ae_fpa_builtins
+  | `Logic (Smtlib2 _) -> bv_builtins ++ smt_fpa_builtins
   | _ -> fun _ _ -> `Not_found
 
 (** Translates dolmen locs to Alt-Ergo's locs *)
@@ -929,6 +1013,13 @@ let mk_add translate sy ty l =
   let args = aux_mk_add l in
   E.mk_term sy args ty
 
+let mk_rounding fpar =
+  let name = Fpa_rounding.string_of_rounding_mode fpar in
+  let ty = Fpa_rounding.fpa_rounding_mode in
+  let sy =
+    Sy.Op (Sy.Constr (Hstring.make name)) in
+  E.mk_term sy [] ty
+
 (** [mk_expr ~loc ~name_base ~toplevel ~decl_kind term]
 
     Builds an Alt-Ergo hashconsed expression from a dolmen term
@@ -1355,6 +1446,15 @@ let rec mk_expr
               | _ -> unsupported "coercion: %a" DE.Term.print term
             end
           | Float, _ -> op Float
+          | AERound(i, j), _ ->
+            let args =
+              let i = E.Ints.of_int i in
+              let j = E.Ints.of_int j in
+              i :: j :: List.map (fun a -> aux_mk_expr a) args in
+            E.mk_term
+              (Sy.Op Float)
+              args
+              (dty_to_ty term_ty)
           | Integer_round, _ -> op Integer_round
           | Abs_real, _ -> op Abs_real
           | Sqrt_real, _ -> op Sqrt_real
@@ -1373,6 +1473,11 @@ let rec mk_expr
           | Not_theory_constant, _ -> op Not_theory_constant
           | Is_theory_constant, _ -> op Is_theory_constant
           | Linear_dependency, _ -> op Linear_dependency
+          | B.RoundNearestTiesToEven, _ -> mk_rounding NearestTiesToEven
+          | B.RoundNearestTiesToAway, _ -> mk_rounding NearestTiesToAway
+          | B.RoundTowardPositive, _ -> mk_rounding Up
+          | B.RoundTowardNegative, _ -> mk_rounding Down
+          | B.RoundTowardZero, _ -> mk_rounding ToZero
           | _, _ -> unsupported "Application Term %a" DE.Term.print term
         end
 
diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
index fe21034b8..d22fcc3db 100644
--- a/src/lib/frontend/typechecker.ml
+++ b/src/lib/frontend/typechecker.ml
@@ -259,18 +259,29 @@ module Env = struct
     | [ x; y ] -> f x y
     | _ -> assert false
 
-  let add_builtin_enum = function
-    | Ty.Tsum (_, cstrs) as ty ->
-      let enum m h =
-        let s = Hstring.view h in
-        MString.add s (`Term (
-            Symbols.Op (Constr h),
-            { args = []; result = ty },
-            Other
-          )) m
-      in
-      fun m -> List.fold_left enum m cstrs
-    | _ -> assert false
+  let add_fpa_enum map =
+    let ty = Fpa_rounding.fpa_rounding_mode in
+    match ty with
+    | Ty.Tsum (_, cstrs) ->
+      List.fold_left
+        (fun m c ->
+           match Fpa_rounding.translate_smt_rounding_mode c with
+           | None ->
+             (* The constructors of the type are expected to be AE rounding
+                modes. *)
+             assert false
+           | Some hs ->
+             MString.add (Hstring.view hs) (`Term (
+                 Symbols.Op (Constr c),
+                 { args = []; result = ty },
+                 Other
+               ))
+               m
+        )
+        map
+        cstrs
+    | _ -> (* Fpa_rounding.fpa_rounding_mode is a sum type. *)
+      assert false
 
   let find_builtin_cstr ty n =
     match ty with
@@ -298,10 +309,12 @@ module Env = struct
     let float prec exp mode x =
       TTapp (Symbols.Op Float, [prec; exp; mode; x])
     in
+    let nte = Fpa_rounding.string_of_rounding_mode NearestTiesToEven in
+    let tname = Fpa_rounding.fpa_rounding_mode_type_name in
     let float32 = float (int "24") (int "149") in
-    let float32d = float32 (mode "NearestTiesToEven") in
+    let float32d = float32 (mode nte) in
     let float64 = float (int "53") (int "1074") in
-    let float64d = float64 (mode "NearestTiesToEven") in
+    let float64d = float64 (mode nte) in
     let op n op profile =
       MString.add n @@ `Term (Symbols.Op op, profile, Other)
     in
@@ -312,8 +325,8 @@ module Env = struct
     let any = Ty.fresh_tvar in
     let env = {
       env with
-      types = Types.add_builtin env.types "fpa_rounding_mode" rm ;
-      builtins = add_builtin_enum Fpa_rounding.fpa_rounding_mode env.builtins;
+      types = Types.add_builtin env.types tname rm ;
+      builtins = add_fpa_enum env.builtins;
     } in
     let builtins =
       env.builtins
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index baf2525a4..a2ba640a8 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -2820,7 +2820,7 @@ let const_view t =
     end
   | { f = Op (Constr c); ty; _ }
     when Ty.equal ty Fpa_rounding.fpa_rounding_mode ->
-    RoundingMode (Fpa_rounding.rounding_mode_of_hs c)
+    RoundingMode (Fpa_rounding.rounding_mode_of_smt_hs c)
   | _ -> Fmt.failwith "unsupported constant: %a" print t
 
 let int_view t =
diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml
index cdd67d3a5..33aabb300 100644
--- a/src/lib/structures/fpa_rounding.ml
+++ b/src/lib/structures/fpa_rounding.ml
@@ -33,64 +33,95 @@ module Hs = Hstring
 module Q = Numbers.Q
 module Z = Numbers.Z
 
+(** The five standard rounding modes of the SMTLIB.
+    Note that the SMTLIB defines these rounding modes to be the only
+    possible modes. *)
 type rounding_mode =
-  (* five standard/why3 fpa rounding modes *)
   | NearestTiesToEven
-  (*ne in Gappa: to nearest, tie breaking to even mantissas*)
-  | ToZero (* zr in Gappa: toward zero *)
-  | Up (* up in Gappa: toward plus infinity *)
-  | Down (* dn in Gappa: toward minus infinity *)
-  | NearestTiesToAway (* na : to nearest, tie breaking away from zero *)
-
-  (* additional Gappa rounding modes *)
-  | Aw (* aw in Gappa: away from zero **)
-  | Od (* od in Gappa: to odd mantissas *)
-  | No (* no in Gappa: to nearest, tie breaking to odd mantissas *)
-  | Nz (* nz in Gappa: to nearest, tie breaking toward zero *)
-  | Nd (* nd in Gappa: to nearest, tie breaking toward minus infinity *)
-  | Nu (* nu in Gappa: to nearest, tie breaking toward plus infinity *)
-
-let pp_rounding_mode ppf m =
-  Format.pp_print_string ppf @@
-  match m with
+  | ToZero
+  | Up
+  | Down
+  | NearestTiesToAway
+
+let cstrs =
+  [
+    NearestTiesToEven;
+    ToZero;
+    Up;
+    Down;
+    NearestTiesToAway;
+  ]
+
+let to_smt_string =
+  function
+  | NearestTiesToEven -> "RNE"
+  | ToZero -> "RTZ"
+  | Up -> "RTP"
+  | Down -> "RTN"
+  | NearestTiesToAway -> "RNA"
+
+let to_ae_string = function
   | NearestTiesToEven -> "NearestTiesToEven"
   | ToZero -> "ToZero"
   | Up -> "Up"
   | Down -> "Down"
   | NearestTiesToAway -> "NearestTiesToAway"
-  | Aw -> "Aw"
-  | Od -> "Od"
-  | No -> "No"
-  | Nz -> "Nz"
-  | Nd -> "Nd"
-  | Nu -> "Nu"
-
-let fpa_rounding_mode, rounding_mode_of_hs =
-  let cstrs =
-    [ (* standards *)
-      NearestTiesToEven;
-      ToZero;
-      Up;
-      Down;
-      NearestTiesToAway;
-      (* non standards *)
-      Aw;
-      Od;
-      No;
-      Nz;
-      Nd;
-      Nu ]
-  in
-  let h_cstrs =
-    List.map (fun c -> Hs.make (Format.asprintf "%a" pp_rounding_mode c)) cstrs
-  in
-  let ty = Ty.Tsum (Hs.make "fpa_rounding_mode", h_cstrs) in
-  let table =
-    let table = Hashtbl.create 17 in
-    List.iter2 (Hashtbl.add table) h_cstrs cstrs;
-    table
-  in
-  ty, Hashtbl.find table
+
+
+let fpa_rounding_mode_ae_type_name = "fpa_rounding_mode"
+
+let fpa_rounding_mode_type_name = "RoundingMode"
+
+(* The exported 'to string' function is the SMT one. *)
+let string_of_rounding_mode = to_smt_string
+
+let hstring_smt_reprs =
+  List.map
+    (fun c -> Hs.make (to_smt_string c))
+    cstrs
+
+let hstring_ae_reprs =
+  List.map
+    (fun c -> Hs.make (to_ae_string c))
+    cstrs
+
+(* The rounding mode is the enum with the SMT values.
+   The Alt-Ergo values are injected in this type. *)
+let fpa_rounding_mode =
+  Ty.Tsum (Hs.make "RoundingMode", hstring_smt_reprs)
+
+let rounding_mode_of_smt_hs =
+  let table = Hashtbl.create 5 in
+  List.iter2 (
+    fun key bnd ->
+      Hashtbl.add table key bnd
+  ) hstring_smt_reprs cstrs;
+  fun key ->
+    try Hashtbl.find table key with
+    | Not_found ->
+      Fmt.failwith
+        "Error while searching for SMT2 FPA value %a."
+        Hstring.print key
+        fpa_rounding_mode_type_name
+
+let rounding_mode_of_ae_hs =
+  let table = Hashtbl.create 5 in
+  List.iter2 (
+    fun key bnd ->
+      Hashtbl.add table key bnd
+  ) hstring_ae_reprs cstrs;
+  fun key ->
+    try Hashtbl.find table key with
+    | Not_found ->
+      Fmt.failwith
+        "Error while searching for Legacy FPA value %a."
+        Hstring.print key
+        fpa_rounding_mode_type_name
+
+let translate_smt_rounding_mode hs =
+  match rounding_mode_of_smt_hs hs with
+  | res -> Some (Hstring.make (to_ae_string res))
+  | exception (Failure _) -> None
 
 (** Helper functions **)
 
@@ -160,9 +191,6 @@ let round_big_int (mode : rounding_mode) y =
     if Q.sign diff = 0 then z
     else if Q.compare diff half < 0 then z else Z.add z (signed_one y)
 
-  | Aw | Od | No | Nz | Nd | Nu -> assert false
-
-
 let to_mantissa_exp prec exp mode x =
   let sign_x = Q.sign x in
   assert ((sign_x = 0) == Q.equal x Q.zero);
diff --git a/src/lib/structures/fpa_rounding.mli b/src/lib/structures/fpa_rounding.mli
index 2aa00eada..956090a9d 100644
--- a/src/lib/structures/fpa_rounding.mli
+++ b/src/lib/structures/fpa_rounding.mli
@@ -28,26 +28,41 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** The rounding modes for the Floating Point Arithmetic theory.
+    In the legacy frontend, the rounding mode type was `fpa_rounding_mode`
+    and defined 5 rounding modes (see the [rounding_mode] type below).
+    The SMT2 standard defines the exact same rounding modes, but with different
+    identifiers. *)
+
 type rounding_mode =
-  (* five standard/why3 fpa rounding modes *)
   | NearestTiesToEven
-  (*ne in Gappa: to nearest, tie breaking to even mantissas*)
-  | ToZero (* zr in Gappa: toward zero *)
-  | Up (* up in Gappa: toward plus infinity *)
-  | Down (* dn in Gappa: toward minus infinity *)
-  | NearestTiesToAway (* na : to nearest, tie breaking away from zero *)
+  | ToZero
+  | Up
+  | Down
+  | NearestTiesToAway
+
+(** Equal to ["RoundingMode"], the SMT2 type of rounding modes. *)
+val fpa_rounding_mode_type_name : string
 
-  (* additional Gappa rounding modes *)
-  | Aw (* aw in Gappa: away from zero **)
-  | Od (* od in Gappa: to odd mantissas *)
-  | No (* no in Gappa: to nearest, tie breaking to odd mantissas *)
-  | Nz (* nz in Gappa: to nearest, tie breaking toward zero *)
-  | Nd (* nd in Gappa: to nearest, tie breaking toward minus infinity *)
-  | Nu (* nu in Gappa: to nearest, tie breaking toward plus infinity *)
+(** Equal to ["fpa_rounding_mode"], the Alt-Ergo native rounding mode type. *)
+val fpa_rounding_mode_ae_type_name : string
 
+(** The rounding mode type. *)
 val fpa_rounding_mode : Ty.t
 
-val rounding_mode_of_hs : Hstring.t -> rounding_mode
+(** Transforms the Hstring corresponding to a RoundingMode element into
+    the [rounding_mode] equivalent. Raises 'Failure' if the string does not
+    correspond to a valid rounding mode. *)
+val rounding_mode_of_smt_hs : Hstring.t -> rounding_mode
+
+(** Same, but for legacy's [rounding_mode] equivalent. *)
+val rounding_mode_of_ae_hs : Hstring.t -> rounding_mode
+
+(** Same, but from AE modes to SMT2 modes. *)
+val translate_smt_rounding_mode : Hstring.t -> Hstring.t option
+
+(** Returns the string representation of the [rounding_mode] (SMT2 standard) *)
+val string_of_rounding_mode : rounding_mode -> string
 
 (** Integer part of binary logarithm for NON-ZERO POSITIVE number **)
 val integer_log_2 : Numbers.Q.t -> int
diff --git a/tests/dune.inc b/tests/dune.inc
index df3c921cd..e165febb3 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -175750,6 +175750,96 @@
 ; Auto-generated part end
 ; File auto-generated by gentests
 
+; Auto-generated part begin
+(subdir float
+  (rule
+   (target test_float3b.fpa_fpa.output)
+   (deps (:input test_float3b.fpa.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --enable-theories fpa
+             %{input})))))))
+  (rule
+   (deps test_float3b.fpa_fpa.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff test_float3b.fpa.expected test_float3b.fpa_fpa.output)))
+  (rule
+   (target test_float3.fpa_fpa.output)
+   (deps (:input test_float3.fpa.ae))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --enable-theories fpa
+             %{input})))))))
+  (rule
+   (deps test_float3.fpa_fpa.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff test_float3.fpa.expected test_float3.fpa_fpa.output)))
+  (rule
+   (target test_float2.models_tableaux.output)
+   (deps (:input test_float2.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver Tableaux
+             %{input})))))))
+  (rule
+   (deps test_float2.models_tableaux.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff test_float2.models.expected test_float2.models_tableaux.output)))
+  (rule
+   (target test_float1.dolmen_dolmen.output)
+   (deps (:input test_float1.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps test_float1.dolmen_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff test_float1.dolmen.expected test_float1.dolmen_dolmen.output))))
+; Auto-generated part end
+; File auto-generated by gentests
+
 ; Auto-generated part begin
 (subdir issues
   (rule
diff --git a/tests/float/test_float1.dolmen.expected b/tests/float/test_float1.dolmen.expected
new file mode 100644
index 000000000..6f99ff0f4
--- /dev/null
+++ b/tests/float/test_float1.dolmen.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/float/test_float1.dolmen.smt2 b/tests/float/test_float1.dolmen.smt2
new file mode 100644
index 000000000..94eb55117
--- /dev/null
+++ b/tests/float/test_float1.dolmen.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+
+(declare-const x Real)
+(assert (> x 0.0))
+(assert (= ((_ ae.round 1 1) RTZ 0.3) x))
+(check-sat)
\ No newline at end of file
diff --git a/tests/float/test_float2.models.expected b/tests/float/test_float2.models.expected
new file mode 100644
index 000000000..e9e394a51
--- /dev/null
+++ b/tests/float/test_float2.models.expected
@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun x () Real (/ 1 4))
+)
diff --git a/tests/float/test_float2.models.smt2 b/tests/float/test_float2.models.smt2
new file mode 100644
index 000000000..1a51c4e27
--- /dev/null
+++ b/tests/float/test_float2.models.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+
+(set-option :produce-models true)
+(declare-const x Real)
+(assert (> x 0.0))
+(assert (= ((_ ae.round 1 2) RTZ 0.3) x))
+(check-sat)
+(get-model)
\ No newline at end of file
diff --git a/tests/float/test_float3.fpa.ae b/tests/float/test_float3.fpa.ae
new file mode 100644
index 000000000..3067a37b5
--- /dev/null
+++ b/tests/float/test_float3.fpa.ae
@@ -0,0 +1,5 @@
+logic x : real
+
+axiom ax : 1.0 <= x
+
+goal g : float(4, 4, NearestTiesToEven, 1.0) <= float(4, 4, NearestTiesToEven, x)
\ No newline at end of file
diff --git a/tests/float/test_float3.fpa.expected b/tests/float/test_float3.fpa.expected
new file mode 100644
index 000000000..6f99ff0f4
--- /dev/null
+++ b/tests/float/test_float3.fpa.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/float/test_float3b.fpa.expected b/tests/float/test_float3b.fpa.expected
new file mode 100644
index 000000000..6f99ff0f4
--- /dev/null
+++ b/tests/float/test_float3b.fpa.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/float/test_float3b.fpa.smt2 b/tests/float/test_float3b.fpa.smt2
new file mode 100644
index 000000000..362ca676e
--- /dev/null
+++ b/tests/float/test_float3b.fpa.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-const x Real)
+(assert (<= 1.0 x))
+(assert (> ((_ ae.round 4 4) RNE 1.0) ((_ ae.round 4 4) RNE x)))
+(check-sat)
\ No newline at end of file