diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala index 8178cc6c821c207054157aa11fc10dd71f9e39c8..bdd5e54d91559676d0a1b8d1e24004d1d7351d23 100644 --- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala +++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala @@ -408,9 +408,16 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) { // TODO: Test output value as well val envMap = bs.map(b => b -> BooleanLiteral(bValues(b))).toMap - val fi = FunctionInvocation(phiFd.typed, ex.ins) - - evaluator.eval(fi, envMap) + ex match { + case InExample(ins) => + val fi = FunctionInvocation(phiFd.typed, ins) + evaluator.eval(fi, envMap) + + case InOutExample(ins, outs) => + val fi = FunctionInvocation(cTreeFd.typed, ins) + val eq = equality(fi, tupleWrap(outs)) + evaluator.eval(eq, envMap) + } } }