diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml
index 36e7bb341..696706c70 100644
--- a/src/lib/reasoners/arith.ml
+++ b/src/lib/reasoners/arith.ml
@@ -813,23 +813,25 @@ module Shostak
         cpt := Q.add Q.one (max_constant distincts !cpt);
         Some (term_of_cst (Q.to_string !cpt), true)
 
-
-
-  let pprint_const_for_model =
-    let pprint_positive_const c =
-      let num = Q.num c in
-      let den = Q.den c in
-      if Z.is_one den then Z.to_string num
-      else Format.sprintf "(/ %s %s)" (Z.to_string num) (Z.to_string den)
-    in
-    fun r ->
-      match P.is_const (embed r) with
-      | None -> assert false
-      | Some c ->
-        let sg = Q.sign c in
-        if sg = 0 then "0"
-        else if sg > 0 then pprint_positive_const c
-        else Format.sprintf "(- %s)" (pprint_positive_const (Q.abs c))
+  let pp_constant ppf r =
+    match P.is_const (embed r), X.type_info r with
+    | Some q, Ty.Tint ->
+      assert (Z.equal (Q.den q) Z.one);
+      let i = Q.num q in
+      if Z.sign i = -1 then
+        Fmt.pf ppf "(- %a)" Z.pp_print (Z.abs i)
+      else
+        Fmt.pf ppf "%a" Z.pp_print i
+    | Some q, Ty.Treal ->
+      if Z.equal (Q.den q) Z.one then
+        Fmt.pf ppf "%a.0" Z.pp_print (Q.num q)
+      else if Q.sign q = -1 then
+        Fmt.pf ppf "(/ (- %a) %a)"
+          Z.pp_print (Z.abs (Q.num q))
+          Z.pp_print (Q.den q)
+      else
+        Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q)
+    | _ -> assert false
 
   let choose_adequate_model t r l =
     if Options.get_debug_interpretation () then
@@ -854,6 +856,6 @@ module Shostak
         List.iter (fun (_,x) -> assert (X.equal x r)) l;
         r
     in
-    r, pprint_const_for_model r
+    r, Fmt.str "%a" pp_constant r
 
 end
diff --git a/src/lib/util/numbers.ml b/src/lib/util/numbers.ml
index c878b3246..8377eed58 100644
--- a/src/lib/util/numbers.ml
+++ b/src/lib/util/numbers.ml
@@ -58,6 +58,7 @@ module Z = struct
   let from_string s = Z.of_string s
   let to_string t   = Z.to_string t
   let print fmt z   = Format.fprintf fmt "%s" (to_string z)
+  let pp_print = Z.pp_print
 
   let my_gcd a b =
     if is_zero a then b
diff --git a/src/lib/util/numbers.mli b/src/lib/util/numbers.mli
index fac3e45b6..a15b41645 100644
--- a/src/lib/util/numbers.mli
+++ b/src/lib/util/numbers.mli
@@ -59,6 +59,7 @@ module Z : sig
   val from_int : int -> t
   val from_string : string -> t
   val to_string : t -> string
+  val pp_print : t Fmt.t
 
   (** convert to machine integer. returns None in case of overflow *)
   val to_machine_int : t -> int option
diff --git a/tests/dune.inc b/tests/dune.inc
index 5179e503e..3a9ff782c 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -176036,6 +176036,28 @@
 
 ; Auto-generated part begin
 (subdir issues
+  (rule
+   (target 926.models_tableaux.output)
+   (deps (:input 926.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 926.models_tableaux.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 926.models.expected 926.models_tableaux.output)))
   (rule
    (target 889_ci_cdcl_no_minimal_bj.output)
    (deps (:input 889.smt2))
diff --git a/tests/issues/926.models.expected b/tests/issues/926.models.expected
new file mode 100644
index 000000000..4c3eea7da
--- /dev/null
+++ b/tests/issues/926.models.expected
@@ -0,0 +1,10 @@
+
+unknown
+(
+  (define-fun x1 () Int 5)
+  (define-fun x2 () Int (- 5))
+  (define-fun y1 () Real (/ 3 2))
+  (define-fun y2 () Real 4.0)
+  (define-fun y3 () Real (/ 16 5))
+  (define-fun y4 () Real (/ (- 3) 2))
+)
diff --git a/tests/issues/926.models.smt2 b/tests/issues/926.models.smt2
new file mode 100644
index 000000000..2c9860dae
--- /dev/null
+++ b/tests/issues/926.models.smt2
@@ -0,0 +1,16 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x1 Int)
+(declare-const x2 Int)
+(declare-const y1 Real)
+(declare-const y2 Real)
+(declare-const y3 Real)
+(declare-const y4 Real)
+(assert (= x1 5))
+(assert (= x2 (- 5)))
+(assert (= y1 (/ (- 3.0) (- 2.0))))
+(assert (= y2 (/ (- 4.0) (- 1.0))))
+(assert (= y3 3.2))
+(assert (= y4 (/ 3.0 (- 2.0))))
+(check-sat)
+(get-model)
diff --git a/tests/models/arith/arith10.optimize.expected b/tests/models/arith/arith10.optimize.expected
index 821c9704f..0431bebaa 100644
--- a/tests/models/arith/arith10.optimize.expected
+++ b/tests/models/arith/arith10.optimize.expected
@@ -1,6 +1,6 @@
 
 unknown
 (
-  (define-fun x () Real 0)
-  (define-fun y () Real 10)
+  (define-fun x () Real 0.0)
+  (define-fun y () Real 10.0)
 )
diff --git a/tests/models/arith/arith11.optimize.expected b/tests/models/arith/arith11.optimize.expected
index 2e6f3872c..81826bf45 100644
--- a/tests/models/arith/arith11.optimize.expected
+++ b/tests/models/arith/arith11.optimize.expected
@@ -1,7 +1,7 @@
 
 unknown
 (
-  (define-fun x () Real 2)
+  (define-fun x () Real 2.0)
   (define-fun p1 () Bool false)
   (define-fun p2 () Bool true)
 )
diff --git a/tests/models/arith/arith5.optimize.expected b/tests/models/arith/arith5.optimize.expected
index 79fc5a3b8..77cec44fe 100644
--- a/tests/models/arith/arith5.optimize.expected
+++ b/tests/models/arith/arith5.optimize.expected
@@ -1,7 +1,7 @@
 
 unknown
 (
-  (define-fun x () Real (- (/ 1 18)))
-  (define-fun y () Real (- (/ 1 36)))
-  (define-fun z () Real (- (/ 7 9)))
+  (define-fun x () Real (/ (- 1) 18))
+  (define-fun y () Real (/ (- 1) 36))
+  (define-fun z () Real (/ (- 7) 9))
 )
diff --git a/tests/models/arith/arith7.optimize.expected b/tests/models/arith/arith7.optimize.expected
index c8aef236f..6c72aa49d 100644
--- a/tests/models/arith/arith7.optimize.expected
+++ b/tests/models/arith/arith7.optimize.expected
@@ -1,10 +1,10 @@
 
 unknown
 (
-  (define-fun x () Real 0)
+  (define-fun x () Real 0.0)
 )
 
 unknown
 (
-  (define-fun x () Real (- (/ 3 2)))
+  (define-fun x () Real (/ (- 3) 2))
 )
diff --git a/tests/models/arith/arith9.optimize.expected b/tests/models/arith/arith9.optimize.expected
index 767881680..419bdb3c3 100644
--- a/tests/models/arith/arith9.optimize.expected
+++ b/tests/models/arith/arith9.optimize.expected
@@ -1,6 +1,6 @@
 
 unknown
 (
-  (define-fun x () Real 4)
-  (define-fun y () Real 4)
+  (define-fun x () Real 4.0)
+  (define-fun y () Real 4.0)
 )