diff --git a/infer/src/base/TaskBar.ml b/infer/src/base/TaskBar.ml
index c5583c818..7e34bb452 100644
--- a/infer/src/base/TaskBar.ml
+++ b/infer/src/base/TaskBar.ml
@@ -17,7 +17,7 @@ let top_bar_size_default = 100
 let min_acceptable_progress_bar = 10
 
 (** infer rulez *)
-let job_prefix = "⊢ "
+let job_prefix = SpecialChars.right_tack ^ " "
 
 (** {2 Task bar} *)
 
diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml
index 1f248cc78..c4481eab1 100644
--- a/infer/src/bufferoverrun/bounds.ml
+++ b/infer/src/bufferoverrun/bounds.ml
@@ -71,7 +71,7 @@ module SymLinear = struct
     in
     if Z.(equal c one) then Symb.Symbol.pp f s
     else if Z.(equal c minus_one) then F.fprintf f "-%a" Symb.Symbol.pp s
-    else F.fprintf f "%a⋅%a" Z.pp_print c Symb.Symbol.pp s
+    else F.fprintf f "%a%s%a" Z.pp_print c SpecialChars.dot_operator Symb.Symbol.pp s
 
 
   let pp : is_beginning:bool -> F.formatter -> t -> unit =
diff --git a/infer/src/bufferoverrun/ints.ml b/infer/src/bufferoverrun/ints.ml
index ae95bdbeb..d2d72a63a 100644
--- a/infer/src/bufferoverrun/ints.ml
+++ b/infer/src/bufferoverrun/ints.ml
@@ -93,11 +93,15 @@ module PositiveInt = struct
 
   let ten = Z.of_int 10
 
-  let exponent_chars = [|"⁰"; "¹"; "²"; "³"; "⁴"; "⁵"; "⁶"; "⁷"; "⁸"; "⁹"|]
-
-  let rec pp_exponent f i =
-    if not Z.(i <= zero) then (
-      let d, r = Z.ediv_rem i ten in
-      pp_exponent f d ;
-      F.pp_print_string f exponent_chars.(Z.to_int r) )
+  let exponent_prefix, exponent_chars = SpecialChars.superscript_digits
+
+  let pp_exponent f i =
+    let rec aux f i =
+      if not Z.(i <= zero) then (
+        let d, r = Z.ediv_rem i ten in
+        aux f d ;
+        F.pp_print_string f exponent_chars.(Z.to_int r) )
+    in
+    F.pp_print_string f exponent_prefix ;
+    aux f i
 end
diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index 3a137dcc7..9a220eb53 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -311,13 +311,16 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
 
   let degree_term p = snd (degree_with_term p)
 
+  let multiplication_sep = F.sprintf " %s " SpecialChars.multiplication_sign
+
   let pp : F.formatter -> t -> unit =
     let add_symb s (((last_s, last_occ) as last), others) =
       if Int.equal 0 (S.compare s last_s) then ((last_s, PositiveInt.succ last_occ), others)
       else ((s, PositiveInt.one), last :: others)
     in
     let pp_coeff fmt (c : NonNegativeInt.t) =
-      if Z.((c :> Z.t) > one) then F.fprintf fmt "%a ⋅ " NonNegativeInt.pp c
+      if Z.((c :> Z.t) > one) then
+        F.fprintf fmt "%a %s " NonNegativeInt.pp c SpecialChars.dot_operator
     in
     let pp_exp fmt (e : PositiveInt.t) =
       if Z.((e :> Z.t) > one) then PositiveInt.pp_exponent fmt e
@@ -329,7 +332,7 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
     let pp_symb fmt symb = pp_magic_parentheses S.pp fmt symb in
     let pp_symb_exp fmt (symb, exp) = F.fprintf fmt "%a%a" pp_symb symb pp_exp exp in
     let pp_symbs fmt (last, others) =
-      List.rev_append others [last] |> Pp.seq ~sep:" × " pp_symb_exp fmt
+      List.rev_append others [last] |> Pp.seq ~sep:multiplication_sep pp_symb_exp fmt
     in
     let rec pp_sub ~print_plus symbs fmt {const; terms} =
       let print_plus =
diff --git a/infer/src/istd/SpecialChars.ml b/infer/src/istd/SpecialChars.ml
new file mode 100644
index 000000000..4cc1dba94
--- /dev/null
+++ b/infer/src/istd/SpecialChars.ml
@@ -0,0 +1,34 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+let utf8 =
+  let rec from_vars = function
+    | [] ->
+        false
+    | var :: otherwise -> (
+      match Sys.getenv var with
+      | Some ("C" | "POSIX") ->
+          false
+      | None | Some "" ->
+          from_vars otherwise
+      | Some lc ->
+          String.is_suffix lc ~suffix:"UTF-8" )
+  in
+  from_vars ["LC_ALL"; "LC_CTYPE"; "LANG"]
+
+
+let dot_operator = if utf8 then "⋅" else "."
+
+let multiplication_sign = if utf8 then "×" else "x"
+
+let right_tack = if utf8 then "⊢" else "|-"
+
+let superscript_digits =
+  if utf8 then ("", [|"⁰"; "¹"; "²"; "³"; "⁴"; "⁵"; "⁶"; "⁷"; "⁸"; "⁹"|])
+  else ("^", [|"0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9"|])
diff --git a/infer/src/istd/SpecialChars.mli b/infer/src/istd/SpecialChars.mli
new file mode 100644
index 000000000..e6cd769ae
--- /dev/null
+++ b/infer/src/istd/SpecialChars.mli
@@ -0,0 +1,16 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+val dot_operator : string
+
+val multiplication_sign : string
+
+val right_tack : string
+
+val superscript_digits : string * string Array.t