diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala index d02804e4584805974aafc5a20792ea2b9ee81cd6..6aeda471b2cde381144e476b0313cf70254f3ff5 100644 --- a/src/main/scala/leon/purescala/Constructors.scala +++ b/src/main/scala/leon/purescala/Constructors.scala @@ -24,4 +24,12 @@ object Constructors { case xs => LetTuple(xs, value, body) } + + def tupleChoose(ch: Choose): Expr = { + if (ch.vars.size > 1) { + ch + } else { + Tuple(Seq(ch)) + } + } } diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala index be878918adf52bc0f3281a4dfada1055b256c533..55e3e685d804c250909b4c35ec0370e349f75903 100644 --- a/src/main/scala/leon/synthesis/ConvertHoles.scala +++ b/src/main/scala/leon/synthesis/ConvertHoles.scala @@ -63,7 +63,7 @@ object ConvertHoles extends LeonPhase[Program, Program] { BooleanLiteral(true) } - val withChoose = letTuple(holes, Choose(cids, pred), newBody) + val withChoose = letTuple(holes, tupleChoose(Choose(cids, pred)), newBody) fd.body = Some(withChoose) } diff --git a/src/main/scala/leon/synthesis/ConvertWithOracles.scala b/src/main/scala/leon/synthesis/ConvertWithOracles.scala index f8072b71a9dedfd1ff50e705607d1f24b1789b57..0d7948e41d46e8e14b6369d1f3e9cd1c1c9a51bd 100644 --- a/src/main/scala/leon/synthesis/ConvertWithOracles.scala +++ b/src/main/scala/leon/synthesis/ConvertWithOracles.scala @@ -54,7 +54,7 @@ object ConvertWithOracle extends LeonPhase[Program, Program] { BooleanLiteral(true) } - Some(letTuple(os, Choose(chooseOs, pred), b)) + Some(letTuple(os, tupleChoose(Choose(chooseOs, pred)), b)) case None => None } diff --git a/src/test/resources/regression/synthesis/Holes/Hole1.scala b/src/test/resources/regression/synthesis/Holes/Hole1.scala index 785271b224098581bcb934c47aa89eb6e081085b..65ff08381086b6318c5da2acece6860f04634f7e 100644 --- a/src/test/resources/regression/synthesis/Holes/Hole1.scala +++ b/src/test/resources/regression/synthesis/Holes/Hole1.scala @@ -3,26 +3,6 @@ import leon.collection._ import leon.lang.synthesis._ object Holes { - def abs1(a: Int) = { - if (?(true, false)) { - a - } else { - -a - } - } ensuring { - _ >= 0 - } - - def abs2(a: Int) = { - if (???[Boolean]) { - a - } else { - -a - } - } ensuring { - _ >= 0 - } - def abs3(a: Int) = { if (?(a > 0, a < 0)) { a