diff --git a/examples/heptreax/README b/examples/heptreax/README
new file mode 100644
index 0000000..3829c93
--- /dev/null
+++ b/examples/heptreax/README
@@ -0,0 +1,18 @@
+Examples of uses of Heptagon with the synthesis tool ReaX.
+
+- Verification (modes.ept, contract without controllable variable) :
+
+heptc -target ctrln modes.ept
+reax -a 'sS:d={P:D}' modes_ctrln/twomodes.ctrln
+
+- Controller synthesis (twomodes.ept, contract with controllable variable) :
+
+heptc -hepts -s twomodes -target c -target ctrln modes.ept
+reax -a 'sS:d={P:D}' --triang modes_ctrln/twomodes.ctrln
+ctrl2ept -n Modes.twomodes
+heptc -target c modes_controller.ept
+gcc -o sim -I/usr/local/lib/heptagon/c -Imodes_c -Imodes_controller_c
+             modes_c/_main.c modes_c/modes.c modes_c/modes_types.c
+             modes_controller_c/modes_controller.c
+             modes_controller_c/modes_controller_types.c
+
diff --git a/examples/heptreax/modes.ept b/examples/heptreax/modes.ept
new file mode 100644
index 0000000..6e4d277
--- /dev/null
+++ b/examples/heptreax/modes.ept
@@ -0,0 +1,20 @@
+node twomodes (v:int) = (o:int)
+
+contract
+  assume (v <= 1) & (v >= 0)
+  enforce (o <= 10) & (o >= 0)
+  with (c:bool)
+  
+var last y : int = 0;
+let
+  o = y;
+  automaton
+    state Up
+      do y = last y + v
+      until not c then Down
+    state Down
+      do y = last y - v
+      until not c then Up
+  end
+tel
+
diff --git a/examples/heptreax/twomodes.ept b/examples/heptreax/twomodes.ept
new file mode 100644
index 0000000..7a06467
--- /dev/null
+++ b/examples/heptreax/twomodes.ept
@@ -0,0 +1,19 @@
+node twomodes (v:int) = (o:int)
+
+contract
+  assume (v <= 1) & (v >= 0)
+  enforce (o <= 10) & (o >= 0)
+
+var last y : int = 0;
+let
+  o = y;
+  automaton
+    state Up
+      do y = last y + v
+      until y >= 10 then Down
+    state Down
+      do y = last y - v
+      until y <= 0 then Up
+  end
+tel
+