diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index df3c1c78af29d587d095a14bcbb321c9b65df9c3..77b34d64ea330dce8ff7f9f3e5c0a4444a00750c 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -77,7 +77,9 @@ trait CodeGeneration {
   private[codegen] val GenericValuesClass        = "leon/codegen/runtime/GenericValues"
   private[codegen] val MonitorClass              = "leon/codegen/runtime/LeonCodeGenRuntimeMonitor"
 
-  def idToSafeJVMName(id: Identifier) = id.uniqueName.replaceAll("\\.", "\\$")
+  def idToSafeJVMName(id: Identifier) = {
+    scala.reflect.NameTransformer.encode(id.uniqueName).replaceAll("\\.", "\\$")
+  }
   def defToJVMName(d : Definition) : String = "Leon$CodeGen$" + idToSafeJVMName(d.id)
 
   /** Retrieve the name of the underlying lazy field from a lazy field accessor method */
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 6f738e6b34bad8afa470de0c49b31e5631280722..4399dc2bfd84fae98155006144b60e7c9a84a114 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -28,7 +28,11 @@ object Common {
     }
   }
 
-  // the type is left blank (Untyped) for Identifiers that are not variables
+  /** Represents a unique symbol in Leon.
+    *
+    * The name is stored in the decoded (source code) form rather than encoded (JVM) form.
+    * The type may be left blank (Untyped) for Identifiers that are not variables.
+    */
   class Identifier private[Common](val name: String, val globalId: Int, val id: Int, val tpe: TypeTree, alwaysShowUniqueID: Boolean = false) extends Tree with Typed {
     self : Serializable =>
 
@@ -83,19 +87,24 @@ object Common {
   }
 
   object FreshIdentifier {
+
+    // Replace $opcode inside a string with the symbolic operator name
+    private def decode(s: String) =
+      scala.reflect.NameTransformer.decode(s)
+
     /** Builds a fresh identifier
       * @param name The name of the identifier
       * @param tpe The type of the identifier
       * @param alwaysShowUniqueID If the unique ID should always be shown */
     def apply(name: String, tpe: TypeTree = Untyped, alwaysShowUniqueID: Boolean = false) : Identifier = 
-      new Identifier(name, UniqueCounter.nextGlobal, UniqueCounter.next(name), tpe, alwaysShowUniqueID)
+      new Identifier(decode(name), UniqueCounter.nextGlobal, UniqueCounter.next(name), tpe, alwaysShowUniqueID)
 
     /** Builds a fresh identifier, whose ID is always shown
       * @param name The name of the identifier
       * @param forceId The forced ID of the identifier
       * @param tpe The type of the identifier */
     def apply(name: String, forceId: Int, tpe: TypeTree): Identifier = 
-      new Identifier(name, UniqueCounter.nextGlobal, forceId, tpe, true)
+      new Identifier(decode(name), UniqueCounter.nextGlobal, forceId, tpe, true)
 
   }
 
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 96881669c621c8baf76d45903278ae6ff16e93a3..1e3722565312e3157de6044351791b49a5235513 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -846,6 +846,7 @@ object Expressions {
   /* Special trees for synthesis */
   /** $encodingof `choose(pred)`, the non-deterministic choice in Leon.
     *
+    * The semantics of this expression is some value
     * @note [[pred]] should be a of a [[Types.FunctionType]].
     */
   case class Choose(pred: Expr) extends Expr {
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 16e36192854ff5bce2ae27564bb00dfc87beb5a7..0014d38766e84b5a75b77859da7bc0974c60d358 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -76,15 +76,7 @@ class PrettyPrinter(opts: PrinterOptions,
         } else {
           id.toString
         }
-        val alphaNumDollar = "[\\w\\$]"
-        // FIXME this does not account for class names with operator symbols
-        def isLegalScalaId(id : String) = id.matches(
-          s"$alphaNumDollar+|[$alphaNumDollar+_]?[!@#%^&*+-\\|~/?><:]+"
-        )
-        // Replace $opname with operator symbols
-        val candidate = scala.reflect.NameTransformer.decode(name)
-
-        if (isLegalScalaId(candidate)) p"$candidate" else p"$name"
+        p"$name"
 
       case Variable(id) =>
         p"$id"
@@ -487,10 +479,7 @@ class PrettyPrinter(opts: PrinterOptions,
         }
 
       case fd: FunDef =>
-        for(a <- fd.annotations) {
-          p"""|@$a
-              |"""
-        }
+        p"${nary(fd.annotations.toSeq, "\n")}"
 
         if (fd.canBeStrictField) {
           p"val ${fd.id} : "
diff --git a/testcases/verification/case-studies/Robot3po.scala b/testcases/verification/case-studies/Robot3po.scala
index c78dc15f2c48703bae470cd41578c7b141d7d9ee..56709fc5555175ede38fac4f00ec6e772ecb9d7d 100644
--- a/testcases/verification/case-studies/Robot3po.scala
+++ b/testcases/verification/case-studies/Robot3po.scala
@@ -661,14 +661,12 @@ object Robot {
          hsts: List[HeatSensorTransition],
          tts: List[TransmitterTransition]): List[RobotTransition] = {
 
-    ets.flatMap { et =>
-      nsts.flatMap { nst =>
-        hsts.flatMap { hst =>
-          tts.map { tt =>
-            RobotTransition(et, nst, hst, tt)
-          }
-        }
-      }
-    }
+    for {
+      et  <- ets
+      nst <- nsts
+      hst <- hsts
+      tt  <- tts
+    } yield RobotTransition(et, nst, hst, tt)
+
   }
 }