diff --git a/src/main/scala/leon/genc/CConverter.scala b/src/main/scala/leon/genc/CConverter.scala index 05a7f2c38fbc057694c7fc8bfa46573d02f6ec0c..a29943083c774f88acbee39ff71490d8104089de 100644 --- a/src/main/scala/leon/genc/CConverter.scala +++ b/src/main/scala/leon/genc/CConverter.scala @@ -413,8 +413,8 @@ class CConverter(val ctx: LeonContext, val prog: Program) { // Transform while (cond) { body } into // while (true) { if (cond) { body } else { break } } val condF = flatten(cond) - val ifelse = condF.body ~~ buildIfElse(condF.value, body, CAST.Break) - CAST.While(CAST.True, ifelse) + val ifelse = condF.body ~~ buildIfElse(condF.value, CAST.NoStmt, CAST.Break) + CAST.While(CAST.True, ifelse ~ body) } case FunctionInvocation(tfd @ TypedFunDef(fd, _), stdArgs) =>