Examples can now call external methods,

both in input and output.
Abstract evaluator returns a regular function invocation if the body could not be evaluated.

src/main/scala/leon/evaluators/AbstractEvaluator.scala

@@ -58,7 +58,7 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu
         case Some(Some((c, mappings))) =>
           e(c.rhs)(rctx.withNewVars(mappings), gctx)
         case _ =>
-          throw RuntimeError("MatchError: "+rscrut.asString+" did not match any of the cases :" + cases)
+          throw RuntimeError("MatchError(Abstract evaluation): "+rscrut.asString+" did not match any of the cases :\n" + cases.mkString("\n"))
       }
 
     case FunctionInvocation(tfd, args) =>
@@ -80,7 +80,11 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu
           (functionInvocation(tfd.fd, evArgsValues), functionInvocation(tfd.fd, evArgsOrigin))
         } else {
           val body = tfd.body.getOrElse(rctx.mappings(tfd.id))
-          e(body)(frame, gctx)
+          try {
+            e(body)(frame, gctx)
+          } catch {
+            case e: RuntimeError => (functionInvocation(tfd.fd, evArgsValues), functionInvocation(tfd.fd, evArgsOrigin))
+          }
         }
       }
       callResult

src/main/scala/leon/synthesis/ExamplesFinder.scala

@@ -18,6 +18,8 @@ import solvers.z3._
 class ExamplesFinder(ctx0: LeonContext, program: Program) {
 
   lazy val evaluator = new DefaultEvaluator(ctx, program)
+  
+  lazy val abstractEvaluator = new AbstractEvaluator(ctx, program)
 
   implicit val ctx = ctx0
 
@@ -160,6 +162,15 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
 
     consolidateTests(allTests)
   }
+  
+  private def expand(e: Expr): Expr=  {
+    abstractEvaluator.eval(e) match {
+      case EvaluationResults.Successful((res, a)) => res
+      case _                                 => e
+    }
+  }
+  
+  private def expand(e: (Expr, Expr)): (Expr, Expr) = (expand(e._1), expand(e._2))
 
   /** Processes ((in, out) passes {
     * cs[=>Case pattExpr if guard => outR]*/
@@ -177,7 +188,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
       // The pattern as expression (input expression)(may contain free variables)
       val (pattExpr, ieMap) = patternToExpression(cs.pattern, in.getType)
       val freeVars = variablesOf(pattExpr).toSeq
-      if (exists(_.isInstanceOf[NoTree])(pattExpr)) {
+      val res = if (exists(_.isInstanceOf[NoTree])(pattExpr)) {
         reporter.warning(cs.pattern.getPos, "Unapply patterns are not supported in IO-example extraction")
         Seq()
       } else if (freeVars.isEmpty) {
@@ -194,8 +205,6 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
             None
         }) getOrElse {
 
-          // If the input contains free variables, it does not provide concrete examples. 
-          // We will instantiate them according to a simple grammar to get them.
           if(this.keepAbstractExamples) {
             cs.optGuard match {
               case Some(BooleanLiteral(false)) =>
@@ -206,6 +215,8 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
                 Seq((Require(pred, pattExpr), cs.rhs))
             }
           } else {
+            // If the input contains free variables, it does not provide concrete examples. 
+            // We will instantiate them according to a simple grammar to get them.
             val dataGen = new GrammarDataGen(evaluator)
 
             val theGuard = replace(Map(in -> pattExpr), cs.optGuard.getOrElse(BooleanLiteral(true)))
@@ -219,6 +230,8 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
           }
         }
       }
+      
+      if(this.keepAbstractExamples) res.map(expand) else res
     }
   }