Add heuristic...

1 files changed, 16 insertions, 0 deletions

diff --git a/tests/source/jeannet.scade b/tests/source/jeannet.scade
new file mode 100644
index 0000000..9fca060
--- /dev/null
+++ b/tests/source/jeannet.scade
@@ -0,0 +1,16 @@
+node test() returns(x, y, probe z: int; a, b: bool)
+var px, py: int;
+let
+  a = false -> pre b;
+  b = true -> not pre a;
+
+  px = pre x;
+  py = pre y;
+
+  x = 0 -> (if a = b then px + 1 else px);
+  y = 0 -> (if a = b then py else py + 1);
+
+  z = x - y;
+
+  guarantee g1: x >= y;
+tel