diff --git a/src/viper/prelude.ml b/src/viper/prelude.ml
index ae9ef64f0a7..f5e500b0021 100644
--- a/src/viper/prelude.ml
+++ b/src/viper/prelude.ml
@@ -48,9 +48,13 @@ adt Option[T] {
   Some(some$0: T)
 }|prelude}
 
+let prelude_text_encoding : string = {prelude|/* Text encoding */
+function $concat(a: Int, b: Int): Int|prelude}
+
 let prelude_typed_references : string = {prelude|/* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
@@ -64,6 +68,7 @@ let prelude reqs: string =
     prelude_array_encoding;
     prelude_tuple_encoding !(reqs.tuple_arities);
     prelude_option_encoding;
+    prelude_text_encoding;
     prelude_typed_references;
     "/* END PRELUDE */"
   ]
diff --git a/src/viper/trans.ml b/src/viper/trans.ml
index 5a52c3df847..6b1df95989d 100644
--- a/src/viper/trans.ml
+++ b/src/viper/trans.ml
@@ -113,6 +113,9 @@ type ctxt =
     ghost_conc : (ctxt -> exp -> exp) list ref;
   }
 
+(* All text literals are injectively mapped into int values *)
+let text_literals : (string, int) Hashtbl.t = Hashtbl.create 32
+
 let add_locals ctxt (locals : (id * T.typ) list) =
   let add (x, t) = Env.add x.it (Local, t) in
   { ctxt with ids = List.fold_right add locals ctxt.ids }
@@ -122,6 +125,17 @@ let self ctxt at =
   | Some id -> !!! at (LocalVar (!!! at id,!!! at RefT))
   | _ -> failwith "no self"
 
+let tr_string_literal at str =
+  let str_id =
+    match Hashtbl.find_opt text_literals str with
+    | None ->
+      let fresh_str_id = Hashtbl.length text_literals in
+      Hashtbl.add text_literals str fresh_str_id;
+      fresh_str_id
+    | Some id -> id
+  in
+  intLitE at str_id
+
 let rec extract_invariants : item list -> (par -> invariants -> invariants) = function
   | [] -> fun _ x -> x
   | { it = InvariantI (s, e); at; _ } :: p ->
@@ -672,8 +686,12 @@ and pat_match ctxt (scrut : M.exp) (p : M.pat) : exp list * (id * T.typ) list *
       let e_scrut = exp ctxt scrut in
       let rhs = !!(IntLitE n) in
       [ !!(EqCmpE (e_scrut, rhs)) ], [], ([], [])
+    | M.TextLit str ->
+      let e_scrut = exp ctxt scrut in
+      let rhs = tr_string_literal p.at str in
+      [ !!(EqCmpE (e_scrut, rhs)) ], [], ([], [])
     | M.PreLit _ -> failwith "Expected PreLit to be eliminated after typing"
-    | _         -> unsupported (p.at) (Arrange.lit !lit)
+    | _          -> unsupported (p.at) (Arrange.lit !lit)
     end
   | M.OptP p' ->
     let e_scrut = exp ctxt scrut in
@@ -812,6 +830,8 @@ and exp ctxt e =
        !!(IntLitE i)
     | M.NullLit ->
        noneE (e.at)
+    | M.TextLit str ->
+      tr_string_literal e.at str
     | _ ->
        unsupported e.at (Arrange.exp e)
     end
@@ -834,6 +854,7 @@ and exp ctxt e =
       | MulOp -> MulE (e1, e2)
       | DivOp -> DivE (e1, e2)
       | ModOp -> ModE (e1, e2)
+      | CatOp -> CallE ("$concat", [e1; e2])
       | _ -> unsupported e.at (Arrange.exp e))
   | M.OrE (e1, e2) ->
      !!(OrE (exp ctxt e1, exp ctxt e2))
@@ -931,6 +952,7 @@ and tr_typ' ctxt typ =
   match typ, T.normalize typ with
   | _, T.Prim T.Int -> IntT
   | _, T.Prim T.Nat -> IntT    (* Viper has no native support for Nat, so translate to Int *)
+  | _, T.Prim T.Text -> IntT   (* Viper has no native support for Text, so translate to uninterpreted Int values *)
   | _, T.Prim T.Bool -> BoolT
   | _, T.Array _ -> ArrayT     (* Viper arrays are not parameterised by element type *)
   | _, T.Opt   t -> OptionT (tr_typ ctxt t)
@@ -962,6 +984,7 @@ and typed_field t =
   | T.Prim T.Int  -> "$int"
   | T.Prim T.Nat  -> "$int"  (* Viper has no native support for Nat, so translate to Int *)
   | T.Prim T.Bool -> "$bool"
+  | T.Prim T.Text -> "$text"
   | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ t)
 
 and array_size_inv at lhs n =
diff --git a/test/repl/ok/viper.stdout.ok b/test/repl/ok/viper.stdout.ok
index 3ce30af4cb8..9379885c3cf 100644
--- a/test/repl/ok/viper.stdout.ok
+++ b/test/repl/ok/viper.stdout.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/array.silicon.ok b/test/viper/ok/array.silicon.ok
index 2aae810e309..283caf9977d 100644
--- a/test/viper/ok/array.silicon.ok
+++ b/test/viper/ok/array.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@39.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@42.1)
diff --git a/test/viper/ok/array.vpr.ok b/test/viper/ok/array.vpr.ok
index 889f66180b3..de41aca78ed 100644
--- a/test/viper/ok/array.vpr.ok
+++ b/test/viper/ok/array.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/assertions.silicon.ok b/test/viper/ok/assertions.silicon.ok
index 0bc36d2a880..3ef74e608d1 100644
--- a/test/viper/ok/assertions.silicon.ok
+++ b/test/viper/ok/assertions.silicon.ok
@@ -1,2 +1,2 @@
-  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@39.13--39.24)
-  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@57.15--57.44)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@42.13--42.24)
+  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@60.15--60.44)
diff --git a/test/viper/ok/assertions.vpr.ok b/test/viper/ok/assertions.vpr.ok
index c9fd9d65ed1..d1d85fdd48f 100644
--- a/test/viper/ok/assertions.vpr.ok
+++ b/test/viper/ok/assertions.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/async.silicon.ok b/test/viper/ok/async.silicon.ok
index 753d4a73cb6..4132895445d 100644
--- a/test/viper/ok/async.silicon.ok
+++ b/test/viper/ok/async.silicon.ok
@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@62.15--62.42)
+  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@65.15--65.42)
diff --git a/test/viper/ok/async.vpr.ok b/test/viper/ok/async.vpr.ok
index 108293945d8..abfde21c192 100644
--- a/test/viper/ok/async.vpr.ok
+++ b/test/viper/ok/async.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/claim-broken.silicon.ok b/test/viper/ok/claim-broken.silicon.ok
index fe4d5b8bbbd..13af7bf74b0 100644
--- a/test/viper/ok/claim-broken.silicon.ok
+++ b/test/viper/ok/claim-broken.silicon.ok
@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@60.20--60.47)
+  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@63.20--63.47)
diff --git a/test/viper/ok/claim-broken.vpr.ok b/test/viper/ok/claim-broken.vpr.ok
index 4a91443c793..10dacb2c038 100644
--- a/test/viper/ok/claim-broken.vpr.ok
+++ b/test/viper/ok/claim-broken.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/claim-reward-naive.vpr.ok b/test/viper/ok/claim-reward-naive.vpr.ok
index 790aca0092c..bfa3dd26762 100644
--- a/test/viper/ok/claim-reward-naive.vpr.ok
+++ b/test/viper/ok/claim-reward-naive.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/claim-simple.silicon.ok b/test/viper/ok/claim-simple.silicon.ok
index 1f9d4f3e52b..eef64e2e302 100644
--- a/test/viper/ok/claim-simple.silicon.ok
+++ b/test/viper/ok/claim-simple.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (claim-simple.vpr@31.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (claim-simple.vpr@34.1)
diff --git a/test/viper/ok/claim-simple.vpr.ok b/test/viper/ok/claim-simple.vpr.ok
index 900e408febf..f14a36dca1a 100644
--- a/test/viper/ok/claim-simple.vpr.ok
+++ b/test/viper/ok/claim-simple.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/claim.vpr.ok b/test/viper/ok/claim.vpr.ok
index fca91d4e149..c1fde4d31b4 100644
--- a/test/viper/ok/claim.vpr.ok
+++ b/test/viper/ok/claim.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/counter.silicon.ok b/test/viper/ok/counter.silicon.ok
index 59f45bc58e6..25cbd81e574 100644
--- a/test/viper/ok/counter.silicon.ok
+++ b/test/viper/ok/counter.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (counter.vpr@31.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (counter.vpr@34.1)
diff --git a/test/viper/ok/counter.vpr.ok b/test/viper/ok/counter.vpr.ok
index 3b8dcff5a59..f31d5da3294 100644
--- a/test/viper/ok/counter.vpr.ok
+++ b/test/viper/ok/counter.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/invariant.silicon.ok b/test/viper/ok/invariant.silicon.ok
index 0c24233b328..9d22ac740ab 100644
--- a/test/viper/ok/invariant.silicon.ok
+++ b/test/viper/ok/invariant.silicon.ok
@@ -1 +1 @@
-  [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@36.13--36.24)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@39.13--39.24)
diff --git a/test/viper/ok/invariant.vpr.ok b/test/viper/ok/invariant.vpr.ok
index 77d25e9bfca..7e70f568d78 100644
--- a/test/viper/ok/invariant.vpr.ok
+++ b/test/viper/ok/invariant.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/label-break-continue.silicon.ok b/test/viper/ok/label-break-continue.silicon.ok
index de726c0062c..a01f038ad0a 100644
--- a/test/viper/ok/label-break-continue.silicon.ok
+++ b/test/viper/ok/label-break-continue.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (label-break-continue.vpr@32.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (label-break-continue.vpr@33.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (label-break-continue.vpr@35.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (label-break-continue.vpr@36.1)
diff --git a/test/viper/ok/label-break-continue.vpr.ok b/test/viper/ok/label-break-continue.vpr.ok
index 0bfabab3f0d..3f4c45054cf 100644
--- a/test/viper/ok/label-break-continue.vpr.ok
+++ b/test/viper/ok/label-break-continue.vpr.ok
@@ -19,9 +19,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/lits.silicon.ok b/test/viper/ok/lits.silicon.ok
index 8bdaa46c364..c78e9d4f25c 100644
--- a/test/viper/ok/lits.silicon.ok
+++ b/test/viper/ok/lits.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (lits.vpr@30.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (lits.vpr@31.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (lits.vpr@33.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (lits.vpr@34.1)
diff --git a/test/viper/ok/lits.vpr.ok b/test/viper/ok/lits.vpr.ok
index 4da08ae3943..d8182ea500d 100644
--- a/test/viper/ok/lits.vpr.ok
+++ b/test/viper/ok/lits.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/loop-invariant.silicon.ok b/test/viper/ok/loop-invariant.silicon.ok
index fbb19f696fa..83b68ad826e 100644
--- a/test/viper/ok/loop-invariant.silicon.ok
+++ b/test/viper/ok/loop-invariant.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (loop-invariant.vpr@30.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (loop-invariant.vpr@31.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (loop-invariant.vpr@33.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (loop-invariant.vpr@34.1)
diff --git a/test/viper/ok/loop-invariant.vpr.ok b/test/viper/ok/loop-invariant.vpr.ok
index a6b9742ffc6..13967df69b9 100644
--- a/test/viper/ok/loop-invariant.vpr.ok
+++ b/test/viper/ok/loop-invariant.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/method-call.silicon.ok b/test/viper/ok/method-call.silicon.ok
index 9e940ad507f..73b9e5cc757 100644
--- a/test/viper/ok/method-call.silicon.ok
+++ b/test/viper/ok/method-call.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (method-call.vpr@31.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (method-call.vpr@34.1)
diff --git a/test/viper/ok/method-call.vpr.ok b/test/viper/ok/method-call.vpr.ok
index 2511b42d77a..ff1a6c5e01f 100644
--- a/test/viper/ok/method-call.vpr.ok
+++ b/test/viper/ok/method-call.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/nats.silicon.ok b/test/viper/ok/nats.silicon.ok
index 5c9bca1234a..f0e971fad6b 100644
--- a/test/viper/ok/nats.silicon.ok
+++ b/test/viper/ok/nats.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (nats.vpr@31.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (nats.vpr@34.1)
diff --git a/test/viper/ok/nats.vpr.ok b/test/viper/ok/nats.vpr.ok
index bab66ac4cfb..3409f8c3549 100644
--- a/test/viper/ok/nats.vpr.ok
+++ b/test/viper/ok/nats.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/odd-even.silicon.ok b/test/viper/ok/odd-even.silicon.ok
index c59b90830f8..8ff9203ce20 100644
--- a/test/viper/ok/odd-even.silicon.ok
+++ b/test/viper/ok/odd-even.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (odd-even.vpr@30.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (odd-even.vpr@31.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (odd-even.vpr@33.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (odd-even.vpr@34.1)
diff --git a/test/viper/ok/odd-even.vpr.ok b/test/viper/ok/odd-even.vpr.ok
index 64298f1d562..e3985b7cc3c 100644
--- a/test/viper/ok/odd-even.vpr.ok
+++ b/test/viper/ok/odd-even.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/option.silicon.ok b/test/viper/ok/option.silicon.ok
index f927a8efee0..06f7bb55f45 100644
--- a/test/viper/ok/option.silicon.ok
+++ b/test/viper/ok/option.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (option.vpr@31.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (option.vpr@34.1)
diff --git a/test/viper/ok/option.vpr.ok b/test/viper/ok/option.vpr.ok
index 3e1445a0c1d..823b20cdf3a 100644
--- a/test/viper/ok/option.vpr.ok
+++ b/test/viper/ok/option.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/polymono.silicon.ok b/test/viper/ok/polymono.silicon.ok
index 463619044bf..94592a8ba3d 100644
--- a/test/viper/ok/polymono.silicon.ok
+++ b/test/viper/ok/polymono.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (polymono.vpr@30.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (polymono.vpr@31.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (polymono.vpr@33.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (polymono.vpr@34.1)
diff --git a/test/viper/ok/polymono.vpr.ok b/test/viper/ok/polymono.vpr.ok
index eabd3c04490..686a90c4c5b 100644
--- a/test/viper/ok/polymono.vpr.ok
+++ b/test/viper/ok/polymono.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/private.vpr.ok b/test/viper/ok/private.vpr.ok
index 0e728d2fc6f..1ffb7653123 100644
--- a/test/viper/ok/private.vpr.ok
+++ b/test/viper/ok/private.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/reverse.silicon.ok b/test/viper/ok/reverse.silicon.ok
index 95bb5bf4431..91ec44fa1b0 100644
--- a/test/viper/ok/reverse.silicon.ok
+++ b/test/viper/ok/reverse.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (reverse.vpr@34.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (reverse.vpr@37.1)
diff --git a/test/viper/ok/reverse.vpr.ok b/test/viper/ok/reverse.vpr.ok
index e55a2beb677..744becfd334 100644
--- a/test/viper/ok/reverse.vpr.ok
+++ b/test/viper/ok/reverse.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/simple-funs.silicon.ok b/test/viper/ok/simple-funs.silicon.ok
index 1859bcafb42..79eb777979e 100644
--- a/test/viper/ok/simple-funs.silicon.ok
+++ b/test/viper/ok/simple-funs.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (simple-funs.vpr@30.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (simple-funs.vpr@31.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (simple-funs.vpr@33.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (simple-funs.vpr@34.1)
diff --git a/test/viper/ok/simple-funs.vpr.ok b/test/viper/ok/simple-funs.vpr.ok
index 2e7344cc17a..d79fba5dff3 100644
--- a/test/viper/ok/simple-funs.vpr.ok
+++ b/test/viper/ok/simple-funs.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/text.silicon.ok b/test/viper/ok/text.silicon.ok
new file mode 100644
index 00000000000..636bc465cdc
--- /dev/null
+++ b/test/viper/ok/text.silicon.ok
@@ -0,0 +1 @@
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (text.vpr@35.1)
diff --git a/test/viper/ok/text.tc.ok b/test/viper/ok/text.tc.ok
new file mode 100644
index 00000000000..3bef35fcb85
--- /dev/null
+++ b/test/viper/ok/text.tc.ok
@@ -0,0 +1,8 @@
+text.mo:5.8-5.19: warning [M0194], unused identifier concat_text (delete or rename to wildcard `_` or `_concat_text`)
+text.mo:13.8-13.18: warning [M0194], unused identifier array_text (delete or rename to wildcard `_` or `_array_text`)
+text.mo:21.8-21.18: warning [M0194], unused identifier tuple_text (delete or rename to wildcard `_` or `_tuple_text`)
+text.mo:32.8-32.17: warning [M0194], unused identifier call_text (delete or rename to wildcard `_` or `_call_text`)
+text.mo:37.8-37.20: warning [M0194], unused identifier change_field (delete or rename to wildcard `_` or `_change_field`)
+text.mo:38.9-38.10: warning [M0194], unused identifier x (delete or rename to wildcard `_` or `_x`)
+text.mo:48.8-48.17: warning [M0194], unused identifier pass_text (delete or rename to wildcard `_` or `_pass_text`)
+text.mo:53.8-53.21: warning [M0194], unused identifier match_on_text (delete or rename to wildcard `_` or `_match_on_text`)
diff --git a/test/viper/ok/text.vpr.ok b/test/viper/ok/text.vpr.ok
new file mode 100644
index 00000000000..0b54cb5b5e8
--- /dev/null
+++ b/test/viper/ok/text.vpr.ok
@@ -0,0 +1,149 @@
+/* BEGIN PRELUDE */
+/* Array encoding */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $loc_inv1(r: Ref): Array
+  function $loc_inv2(r: Ref): Int
+  axiom $all_diff_array { forall a: Array, i: Int :: {$loc(a, i)} $loc_inv1($loc(a, i)) == a && $loc_inv2($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
+define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+/* Tuple encoding */
+adt Tuple$2 [T0, T1] { Tup$2(tup$2$0 : T0, tup$2$1 : T1) }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
+/* Typed references */
+field $int: Int
+field $bool: Bool
+field $text: Int
+field $ref: Ref
+field $array: Array
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+/* END PRELUDE */
+
+define $Perm($Self) (((true && acc(($Self).fld1,write)) && acc(($Self).fld2,write)))
+define $Inv($Self) (true)
+method __init__($Self: Ref)
+    
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      ($Self).fld1 := 4;
+      ($Self).fld2 := 4; 
+    }
+field fld1: Int
+field fld2: Int
+method concat_text($Self: Ref)
+    
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { var x: Int
+      var y: Int
+      var z: Int
+      x := 0;
+      y := 1;
+      z := $concat(x, y);
+      assert (z == $concat(0, 1));
+      label $Ret; 
+    }
+method array_text($Self: Ref)
+    
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { var arr: Array
+      inhale $array_acc(arr, $text, write);
+      inhale ($size(arr) == 2);
+      ($loc(arr, 0)).$text := 2;
+      ($loc(arr, 1)).$text := 2;
+      ($loc(arr, 0)).$text := 0;
+      ($loc(arr, 1)).$text := 1;
+      assert ((($loc(arr, 0)).$text == 0) && (($loc(arr, 1)).$text == 1));
+      label $Ret; 
+    }
+method tuple_text($Self: Ref)
+    
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { var tup: Tuple$2[Int, Int]
+      tup := Tup$2(0, 1);
+      assert (((tup).tup$2$0 == 0) && ((tup).tup$2$1 == 1));
+      label $Ret; 
+    }
+method get_text($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures ($Res == 0)
+    { 
+      $Res := 0;
+      goto $Ret;
+      label $Ret; 
+    }
+method call_text($Self: Ref)
+    
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { var res: Int
+      res := get_text($Self);
+      assert (res == 0);
+      label $Ret; 
+    }
+method text_arg($Self: Ref, txt: Int)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires (txt == 3)
+    ensures $Perm($Self)
+    ensures ($Res == $concat(3, 4))
+    { 
+      $Res := $concat(txt, 4);
+      goto $Ret;
+      label $Ret; 
+    }
+method pass_text($Self: Ref)
+    
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { var res: Int
+      res := text_arg($Self, 3);
+      assert (res == $concat(3, 4));
+      label $Ret; 
+    }
+method match_on_text($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures ($Res == 42)
+    { var txt: Int
+      txt := get_text($Self);
+      if ((txt == 0))
+         { 
+           $Res := 42;
+           goto $Ret; 
+         }else
+         { 
+           if ((txt == 1))
+              { 
+                $Res := 100;
+                goto $Ret; 
+              }else
+              { 
+                if (true)
+                   { 
+                     $Res := 0;
+                     goto $Ret; 
+                   }; 
+              }; 
+         };
+      label $Ret; 
+    }
diff --git a/test/viper/ok/text.vpr.stderr.ok b/test/viper/ok/text.vpr.stderr.ok
new file mode 100644
index 00000000000..3bef35fcb85
--- /dev/null
+++ b/test/viper/ok/text.vpr.stderr.ok
@@ -0,0 +1,8 @@
+text.mo:5.8-5.19: warning [M0194], unused identifier concat_text (delete or rename to wildcard `_` or `_concat_text`)
+text.mo:13.8-13.18: warning [M0194], unused identifier array_text (delete or rename to wildcard `_` or `_array_text`)
+text.mo:21.8-21.18: warning [M0194], unused identifier tuple_text (delete or rename to wildcard `_` or `_tuple_text`)
+text.mo:32.8-32.17: warning [M0194], unused identifier call_text (delete or rename to wildcard `_` or `_call_text`)
+text.mo:37.8-37.20: warning [M0194], unused identifier change_field (delete or rename to wildcard `_` or `_change_field`)
+text.mo:38.9-38.10: warning [M0194], unused identifier x (delete or rename to wildcard `_` or `_x`)
+text.mo:48.8-48.17: warning [M0194], unused identifier pass_text (delete or rename to wildcard `_` or `_pass_text`)
+text.mo:53.8-53.21: warning [M0194], unused identifier match_on_text (delete or rename to wildcard `_` or `_match_on_text`)
diff --git a/test/viper/ok/tuple.silicon.ok b/test/viper/ok/tuple.silicon.ok
index 9952c657f63..5662a29c2d5 100644
--- a/test/viper/ok/tuple.silicon.ok
+++ b/test/viper/ok/tuple.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (tuple.vpr@36.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (tuple.vpr@39.1)
diff --git a/test/viper/ok/tuple.vpr.ok b/test/viper/ok/tuple.vpr.ok
index d7b2d108d82..8b3a614c418 100644
--- a/test/viper/ok/tuple.vpr.ok
+++ b/test/viper/ok/tuple.vpr.ok
@@ -22,9 +22,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/ok/unsupported.vpr.stderr.ok b/test/viper/ok/unsupported.vpr.stderr.ok
index 39fd5aabddc..7003544e4a6 100644
--- a/test/viper/ok/unsupported.vpr.stderr.ok
+++ b/test/viper/ok/unsupported.vpr.stderr.ok
@@ -1,4 +1,4 @@
 unsupported.mo:5.7-5.8: warning [M0194], unused identifier x (delete or rename to wildcard `_` or `_x`)
-(unknown location): viper error [0], translation to viper failed:
-(Prim Text)
+unsupported.mo:5.17-5.20: viper error [0], translation to viper failed:
+(LitE (CharLit 97))
 
diff --git a/test/viper/ok/variants.silicon.ok b/test/viper/ok/variants.silicon.ok
index c11c148b3a0..0d0474b877d 100644
--- a/test/viper/ok/variants.silicon.ok
+++ b/test/viper/ok/variants.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (variants.vpr@30.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (variants.vpr@31.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (variants.vpr@33.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (variants.vpr@34.1)
diff --git a/test/viper/ok/variants.vpr.ok b/test/viper/ok/variants.vpr.ok
index ff97b131f58..403b2e27117 100644
--- a/test/viper/ok/variants.vpr.ok
+++ b/test/viper/ok/variants.vpr.ok
@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
diff --git a/test/viper/text.mo b/test/viper/text.mo
new file mode 100644
index 00000000000..62d4590ea40
--- /dev/null
+++ b/test/viper/text.mo
@@ -0,0 +1,63 @@
+actor Text {
+  let fld1 = "42";
+  var fld2 = "42";
+
+  func concat_text() {
+    let x = "foo";
+    let y = "bar";
+    let z = x # y;
+
+    assert:system z == "foo" # "bar";
+  };
+
+  func array_text() {
+    let arr: [var Text] = [var "", ""];
+    arr[0] := "foo";
+    arr[1] := "bar";
+
+    assert:system arr[0] == "foo" and arr[1] == "bar";
+  };
+
+  func tuple_text() {
+    let tup: (Text, Text) = ("foo", "bar");
+
+    assert:system tup.0 == "foo" and tup.1 == "bar";
+  };
+
+  func get_text(): Text {
+    assert:return (var:return) == "foo";
+    return "foo";
+  };
+
+  func call_text() {
+    let res = get_text();
+    assert:system res == "foo";
+  };
+
+  func change_field(): async () {
+    let x = fld1;
+    fld2 := "1000";
+  };
+
+  func text_arg(txt: Text): Text {
+    assert:func txt == "abc";
+    assert:return (var:return) == "abc" # "42";
+    return txt # "42";
+  };
+
+  func pass_text() {
+    let res = text_arg("abc");
+    assert:system res == "abc" # "42";
+  };
+
+  func match_on_text(): Int {
+    assert:return (var:return) == 42;
+
+    let txt = get_text();
+    switch txt {
+      case "foo" return 42;
+      case "bar" return 100;
+      case _ return 0;
+    }
+  };
+}
diff --git a/test/viper/unsupported.mo b/test/viper/unsupported.mo
index 1dcec99779f..a1edd67590a 100644
--- a/test/viper/unsupported.mo
+++ b/test/viper/unsupported.mo
@@ -2,6 +2,6 @@
 
 actor {
 
-  let x = ""; // strings aren't supported
+  let x: Char = 'a'; // chars aren't supported
 
 }