diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 5fd73851864805fd8b9e804b17f944fb3f71d5db..f0b7d5f91a9f53f32dd6eb9590c988618f0536d4 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -607,15 +607,15 @@ trait AbstractZ3Solver extends Solver {
               case _ =>
                 reporter.fatalError("Unexpected target type for BV value: " + tpe.asString)
             }
-          } else       
-          _root_.smtlib.common.Hexadecimal.fromString(t.toString.substring(2)) match {
+          } else {  
+            _root_.smtlib.common.Hexadecimal.fromString(t.toString.substring(2)) match {
               case Some(hexa) =>
                 tpe match {
                   case Int32Type => IntLiteral(hexa.toInt)
                   case CharType  => CharLiteral(hexa.toInt.toChar)
                   case _ => unsound(t, "unexpected target type for BV value: " + tpe.asString)
                 }
-            case None => unsound(t, "could not translate Z3NumeralIntAST numeral")
+              case None => unsound(t, "could not translate Z3NumeralIntAST numeral")
             }
           }
 
diff --git a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
index 51e88cfef72acddc85c2ee503a5ba4e68d1adcba..cfe8f456aac42684be263b5594d151fd463e1623 100644
--- a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
@@ -58,7 +58,7 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
         }
       case None =>
         val id = FreshIdentifier("res", fd.returnType, false)
-        fd.postcondition = Some(Lambda(Seq(ValDef(id, None)), Passes(inputVariables, Variable(id), newCases)))
+        fd.postcondition = Some(Lambda(Seq(ValDef(id, false)), Passes(inputVariables, Variable(id), newCases)))
         //ctx0.reporter.info("No postcondition, adding it: " + fd)
     }
     fd.body match { // TODO: Is it correct to discard the choose construct inside the body?
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 3604808df22992888cb7ed9b01843530ad690f95..d5c0b21e64e7f846fc5f829b0f6e5b10065fbf9f 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -325,7 +325,7 @@ case object StringRender extends Rule("StringRender") {
       : (Stream[WithIds[MatchCase]], StringSynthesisResult) = cct match {
       case CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2) =>
         val typeMap = tparams.zip(tparams2).toMap
-        val fields = ccd.fields.map(vd => TypeOps.instantiateType(vd, typeMap).id )
+        val fields = ccd.fields.map(vd => TypeOps.instantiateType(vd.id, typeMap) )
         val pattern = CaseClassPattern(None, ccd.typed(tparams2), fields.map(k => WildcardPattern(Some(k))))
         val (rhs, result) = createFunDefsTemplates(ctx.copy(currentCaseClassParent=Some(cct)), fields.map(Variable)) // Invoke functions for each of the fields.
         val newCases = rhs.map(e => (MatchCase(pattern, None, e._1), e._2))
@@ -351,7 +351,7 @@ case object StringRender extends Rule("StringRender") {
       val cases = (ListBuffer[WithIds[MatchCase]]() /: act.knownCCDescendants) {
         case (acc, cct@CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2)) =>
           val typeMap = tparams.zip(tparams2).toMap
-          val fields = ccd.fields.map(vd => TypeOps.instantiateType(vd, typeMap).id )
+          val fields = ccd.fields.map(vd => TypeOps.instantiateType(vd.id, typeMap) )
           val pattern = CaseClassPattern(None, ccd.typed(tparams2), fields.map(k => WildcardPattern(Some(k))))
           val rhs = StringLiteral(id.asString)
           MatchCase(pattern, None, rhs)