diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala index 1c562d887c4338e1db90fee5af8c98c0e011bac6..cfd3cf6d55d0144a4035aeccda161e340adad9ad 100644 --- a/src/main/scala/leon/synthesis/ExamplesFinder.scala +++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala @@ -57,7 +57,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) { def isValidTest(e: Example): Boolean = { e match { case InOutExample(ins, outs) => - evaluator.eval(Equals(outs.head, FunctionInvocation(fd.typed(fd.tparams.map(_.tp)), ins))) match { + evaluator.eval(Equals(outs.head, FunctionInvocation(fd.typed, ins))) match { case EvaluationResults.Successful(BooleanLiteral(true)) => true case _ => false } diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala index b8a41fdf7309e1cd05274055d3eca3cf4795bc41..6f340554da971b0d833fe3c27998ab39540d21ee 100644 --- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala +++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala @@ -596,7 +596,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) { def solveForTentativeProgram(): Option[Option[Set[Identifier]]] = { val solverf = SolverFactory.getFromSettings(hctx, programCTree).withTimeout(exSolverTo) val solver = solverf.getNewSolver() - val cnstr = FunctionInvocation(phiFd.typed, phiFd.params.map(_.id.toVariable)) + val cnstr = phiFd.applied //println("Program: ") //println("-"*80)