diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala index 0b740adf716f9a805e807e8fa2a561b7879f0044..7ced27bff9fbcbfce0c6af67e4b8e916ebe1c69d 100644 --- a/src/main/scala/leon/synthesis/rules/Cegis.scala +++ b/src/main/scala/leon/synthesis/rules/Cegis.scala @@ -240,7 +240,7 @@ abstract class CEGISLike(name: String) extends Rule(name) { val forArray = replace(substMap, simplerRes) // We trust arrays to be fast... - val eval = evaluator.compile(forArray, ba +: p.as) + val eval = evaluator.compile(matchToIfThenElse(forArray), ba +: p.as) eval.map{e => { case (bss, ins) => e(FiniteArray(bss).setType(ArrayType(BooleanType)) +: ins) @@ -248,7 +248,7 @@ abstract class CEGISLike(name: String) extends Rule(name) { } def compileWithArgs(): Option[(Seq[Expr], Seq[Expr]) => EvaluationResult] = { - val eval = evaluator.compile(simplerRes, bssOrdered ++ p.as) + val eval = evaluator.compile(matchToIfThenElse(simplerRes), bssOrdered ++ p.as) eval.map{e => { case (bss, ins) => e(bss ++ ins)