Added pretty printing for any function ending with "toString" (any case) of the right type,

for displaying counter-examples for the Verification.

src/main/scala/leon/verification/VerificationCondition.scala

@@ -4,10 +4,12 @@ package leon.verification
 
 import leon.purescala.Expressions._
 import leon.purescala.Definitions._
+import leon.purescala.Types._
 import leon.purescala.PrettyPrinter
 import leon.utils.Positioned
-
+import leon.evaluators.StringTracingEvaluator
 import leon.solvers._
+import leon.LeonContext
 
 /** This is just to hold some history information. */
 case class VC(condition: Expr, fd: FunDef, kind: VCKind) extends Positioned {
@@ -44,6 +46,26 @@ case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option
   def isInvalid = status.isInstanceOf[VCStatus.Invalid]
   def isInconclusive = !isValid && !isInvalid
 
+  def userDefinedString(v: Expr, orElse: =>String)(vctx: VerificationContext): String = {
+    //println(vctx.program.definedFunctions.map(fd => fd.id.name + "," + (fd.returnType == StringType) + ", " + (fd.params.length == 1) + "," + (fd.params.length == 1 && fd.params.head.getType == v.getType)).mkString("\n"))
+    (vctx.program.definedFunctions find {
+      case fd => fd.returnType == StringType && fd.params.length == 1 && fd.params.head.getType == v.getType && fd.id.name.toLowerCase().endsWith("tostring")
+    }) match {
+      case Some(fd) =>
+        println("Found fd: " + fd.id.name)
+        val ste = new StringTracingEvaluator(vctx.context, vctx.program)
+        val result = ste.eval(FunctionInvocation(fd.typed, Seq(v)))
+        result.result match {
+          case Some((StringLiteral(res), _)) =>
+            res
+          case _ =>
+            orElse
+        }
+      case None =>
+        orElse
+    }
+  }
+  
   def report(vctx: VerificationContext) {
     import vctx.reporter
     import vctx.context
@@ -60,7 +82,8 @@ case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option
         // large arrays faithfully in ScalaPrinter is hard, while PrettyPrinter
         // is free to simplify
         val strings = cex.toSeq.sortBy(_._1.name).map {
-          case (id, v) => (id.asString(context), PrettyPrinter(v))
+          case (id, v) =>
+            (id.asString(context), userDefinedString(v, PrettyPrinter(v))(vctx))
         }
 
         if (strings.nonEmpty) {