diff --git a/src/model/real.ml b/src/model/real.ml
index 0f201645c..74f48bf84 100644
--- a/src/model/real.ml
+++ b/src/model/real.ml
@@ -92,6 +92,7 @@ let builtins ~eval env (cst : Dolmen.Std.Expr.Term.Const.t) =
   | B.Modulo_f `Real -> op2 ~cst mod_f
   | B.Is_rat `Real -> Some (Bool.mk true)
   | B.Floor `Real -> op1 ~cst floor
+  | B.Floor_to_int `Real -> Some (fun1 ~cst (fun x -> Int.mk (Int.floor x)))
   | B.Ceiling `Real -> op1 ~cst ceil
   | B.Truncate `Real -> op1 ~cst truncate
   | B.Round `Real -> op1 ~cst round
diff --git a/tests/model/coercion/dune b/tests/model/coercion/dune
index c08c489ff..f14a89d52 100644
--- a/tests/model/coercion/dune
+++ b/tests/model/coercion/dune
@@ -33,4 +33,36 @@
   (action (diff int_to_real.expected int_to_real.full)))
 
 
+; Test for real_to_int.smt2
+; Incremental test
+
+(rule
+   (target  real_to_int.incremental)
+   (deps    (:response real_to_int.rsmt2) (:input real_to_int.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff real_to_int.expected real_to_int.incremental)))
+
+; Full mode test
+
+(rule
+   (target  real_to_int.full)
+   (deps    (:response real_to_int.rsmt2) (:input real_to_int.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff real_to_int.expected real_to_int.full)))
+
+
 ; Auto-generated part end
diff --git a/tests/model/coercion/real_to_int.expected b/tests/model/coercion/real_to_int.expected
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/model/coercion/real_to_int.rsmt2 b/tests/model/coercion/real_to_int.rsmt2
new file mode 100644
index 000000000..f19498b12
--- /dev/null
+++ b/tests/model/coercion/real_to_int.rsmt2
@@ -0,0 +1,4 @@
+sat
+(
+  (define-fun x () Real 2.2)
+)
diff --git a/tests/model/coercion/real_to_int.smt2 b/tests/model/coercion/real_to_int.smt2
new file mode 100644
index 000000000..305a30aac
--- /dev/null
+++ b/tests/model/coercion/real_to_int.smt2
@@ -0,0 +1,6 @@
+(set-option :produce-models)
+(set-logic QF_LIRA)
+(declare-const x Real)
+(assert (= (to_int x) 2))
+(check-sat)
+(get-model)