diff --git a/testcases/testgen/ImpWaypoint.scala b/testcases/testgen/ImpWaypoint.scala new file mode 100644 index 0000000000000000000000000000000000000000..932d362b6faada0d8acf684d96d6bcaada0cca21 --- /dev/null +++ b/testcases/testgen/ImpWaypoint.scala @@ -0,0 +1,20 @@ + +import leon.Utils._ +import leon.Annotations._ + +object Imp { + + @main + def foo(i: Int): Int = { + var a = 0 + a = a + 3 + if(i < a) + waypoint(1, a = a + 1) + else + a = a - 1 + a + } ensuring(_ >= 0) + +} + +// vim: set ts=4 sw=4 et: