From 9ca8bcb35eb0385c8f9852045bb282c445bd6901 Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Thu, 10 Jul 2014 18:01:28 +0200
Subject: Add heuristic...

---
 tests/source/jeannet.scade | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 tests/source/jeannet.scade

(limited to 'tests')

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
-- 
cgit v1.2.3