FunDef.postOrTrue

src/main/scala/leon/purescala/Definitions.scala

@@ -394,6 +394,10 @@ object Definitions {
     def postcondition_=(op: Option[Expr]) = {
       fullBody = withPostcondition(fullBody, op) 
     }
+    def postOrTrue = postcondition getOrElse {
+      val arg = ValDef(FreshIdentifier("res", returnType, alwaysShowUniqueID = true))
+      Lambda(Seq(arg), BooleanLiteral(true))
+    }
 
     def hasBody          = body.isDefined
     def hasPrecondition  = precondition.isDefined

src/main/scala/leon/repair/Repairman.scala

@@ -129,9 +129,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
 
     val origBody = fd.body.get
 
-    val spec = fd.postcondition.getOrElse(
-      Lambda(Seq(ValDef(FreshIdentifier("res", fd.returnType))), BooleanLiteral(true))
-    )
+    val spec = fd.postOrTrue
 
     val choose = Choose(spec)