From a0d66baa016378830bf0955260353e1cc8fbcf22 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com> Date: Tue, 26 Jun 2012 19:19:50 +0200 Subject: [PATCH] one more test --- testcases/testgen/ImpWaypoint.scala | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 testcases/testgen/ImpWaypoint.scala diff --git a/testcases/testgen/ImpWaypoint.scala b/testcases/testgen/ImpWaypoint.scala new file mode 100644 index 000000000..932d362b6 --- /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: -- GitLab