diff --git a/test/CTestTestfile.cmake b/test/CTestTestfile.cmake
index 4bce712..dd5684b 100644
--- a/test/CTestTestfile.cmake
+++ b/test/CTestTestfile.cmake
@@ -965,6 +965,11 @@ ADD_TEST(compile_javac_run_tuple_args "scripts/compile_javac_run" "good/tuple_ar
 ADD_TEST(compile_javac_run_type_alias "scripts/compile_javac_run" "good/type_alias.ept")
 ADD_TEST(compile_javac_run_updown "scripts/compile_javac_run" "good/updown.ept")
 ADD_TEST(compile_javac_run_when_merge1 "scripts/compile_javac_run" "good/when_merge1.ept")
+ADD_TEST(compile_sdc_run_alloc "scripts/compile_sdc_run" "sdc/alloc.ept")
+ADD_TEST(compile_sdc_run_lnum_simple "scripts/compile_sdc_run" "sdc/lnum_simple.ept")
 ADD_TEST(compile_sdc_run_modular "scripts/compile_sdc_run" "sdc/modular.ept")
 ADD_TEST(compile_sdc_run_office "scripts/compile_sdc_run" "sdc/office.ept")
+ADD_TEST(compile_sdc_run_optim "scripts/compile_sdc_run" "sdc/optim.ept")
+ADD_TEST(compile_sdc_run_radiotrans "scripts/compile_sdc_run" "sdc/radiotrans.ept")
+ADD_TEST(compile_sdc_run_servers "scripts/compile_sdc_run" "sdc/servers.ept")
 ADD_TEST(compile_sdc_run_tracking "scripts/compile_sdc_run" "sdc/tracking.ept")
diff --git a/test/sdc/alloc.ept b/test/sdc/alloc.ept
new file mode 100644
index 0000000..e6f79ac
--- /dev/null
+++ b/test/sdc/alloc.ept
@@ -0,0 +1,51 @@
+node alloc(r,e : bool) returns (g : bool)
+let
+  automaton
+    state Idle
+      do g = false until r then Alloc
+    state Alloc
+      do g = true until e then Idle
+  end
+tel
+
+node main_alloc(r1,r2,e1,e2 : bool) returns (g1,g2 : bool)
+    contract
+    assume not (r1 & r2)
+    enforce not (g1 & g2)
+    with (c1,c2:bool)
+let
+  g1 = inlined alloc(r1 & c1, e1);
+  g2 = inlined alloc(r2 & c2, e2);
+tel
+
+node task<<pr,pe:int>>() returns (r,e:bool)
+let
+    automaton
+    state I
+      var c : int;
+    do
+      r = c = pr;
+      e = false;
+      c = 1 fby c + 1
+    until r then A
+    state A
+        var c : int;
+    do
+      r = false;
+      e = c = pe;
+      c = 1 fby c + 1;
+    until e then I
+    end
+tel
+    
+(* CHECK main *)
+
+node main() returns (ok:bool)
+var r1,r2,e1,e2,g1,g2:bool;
+let
+  (g1,g2) = main_alloc(r1,r2 & not r1,e1,e2);
+  (* task 1 *)
+  (r1,e1) = task<<5,15>>();
+  (r2,e2) = task<<11,27>>();
+  ok = not (g1 & g2);
+tel
diff --git a/test/sdc/lnum_simple.ept b/test/sdc/lnum_simple.ept
new file mode 100644
index 0000000..a304d41
--- /dev/null
+++ b/test/sdc/lnum_simple.ept
@@ -0,0 +1,47 @@
+(* SDC sS:d={P:D} *)
+
+node f(x:int) = (y:int)
+  contract
+  assume x >= 10
+  enforce y <= x
+  with (c:bool)
+let
+  y = 0 -> if c then pre y + 1 else 0;
+tel
+
+
+node tasks(nb_req, ended : int) = (waiting, active : int)
+      contract
+      assume (nb_req >= 0) & (ended <= (0 fby active)) & (ended >= 0)
+      enforce (active <= 10)
+      with (act : bool)
+var activated : int;
+let
+  waiting = (0 -> pre waiting) + nb_req - activated;
+  activated = 0 -> if (pre waiting > 0) & act then 1 else 0;
+  active = (0 -> pre active) + activated - ended;
+tel  
+
+node period<<n:int>>() = (s:bool)
+var c:int;
+let
+  c = 1 fby (if s then 1 else c + 1);
+  s = c = n;
+tel
+
+fun min(x,y:int) = (z:int)
+let
+    z = if x < y then x else y;
+tel
+
+node main() = (ok:bool;active,ended:int)
+contract assume (active >= 0) & (ended <= (0 fby active)) & (ended >= 0)
+var x,y,nb_req,waiting:int;
+let
+  y = f(x);
+  x = 20;
+  nb_req = 0 -> if (pre waiting < 100) & period<<17>>() then 23 else 0;
+  ended = 0;
+  (waiting,active) = tasks(nb_req,ended);
+  ok = (y <= x) & (active <= 9)
+tel
diff --git a/test/sdc/modular.ept b/test/sdc/modular.ept
index 72c1b0c..260f8a3 100644
--- a/test/sdc/modular.ept
+++ b/test/sdc/modular.ept
@@ -27,6 +27,7 @@ let
     z = f(u & c, m)
 tel
 
+(* CHECK main *)
 node main() = (ok:bool)
 var u : bool;
     m : t;
diff --git a/test/sdc/optim.ept b/test/sdc/optim.ept
new file mode 100644
index 0000000..6deb3ea
--- /dev/null
+++ b/test/sdc/optim.ept
@@ -0,0 +1,24 @@
+node f(x:bool) = (last y:int)
+  contract
+  enforce y > 0 with (c:bool)
+let
+    automaton
+    state A
+    do y = 1;
+    until  c then B
+    | not c then C
+    state B
+    do y = 2;
+    until true then A
+    state C
+    do y = 3;
+    until true then A
+    end
+tel
+
+
+node main() = (y:int)
+let
+    y = f(true)
+tel
+    
diff --git a/test/sdc/radiotrans.ept b/test/sdc/radiotrans.ept
new file mode 100644
index 0000000..03bdcd7
--- /dev/null
+++ b/test/sdc/radiotrans.ept
@@ -0,0 +1,141 @@
+  (* Example from Nicolas Berthier *)
+
+node transceiver(enter_tx,
+		 enter_rx,
+		 exit_rx,
+		 calibrate,
+		 sleep,
+		 wake_up,
+		 irq_tx_done,
+		 irq_on_packet,
+		 irq_end_of_packet,
+		 irq_end_of_calibration,
+		 irq_fifo_threshold,
+		 ok:bool) returns (red:bool)
+let
+  automaton
+    state Idle
+      do
+	red = false;
+      until enter_tx & ok then Tx
+          | calibrate & ok then Calibrate
+          | sleep & ok then Sleep
+          | enter_rx & ok then Rx
+    state Tx
+      do
+	red = true;
+      until irq_tx_done then Idle
+    state Calibrate
+      do
+	red = false;
+      until irq_end_of_calibration then Idle
+    state Sleep
+      do
+	red = false;
+      until wake_up & ok then Idle
+    state Rx
+      do
+	red = true;
+      until irq_on_packet then Rx_Packet
+          | exit_rx & ok then Idle
+    state Rx_Packet
+      do
+	red = true;
+      until irq_end_of_packet then Idle
+  end
+tel
+
+node adc(adc_on,adc_off,ok:bool) returns (o:bool)
+let
+  automaton
+    state Off
+      do
+	o = false;
+      until adc_on & ok then On
+    state On
+      do
+	o = true;
+      until adc_off & ok then Off
+  end
+tel
+
+node main_rt(enter_tx,
+	     enter_rx,
+	     exit_rx,
+	     calibrate,
+	     sleep,
+	     wake_up,
+	     irq_tx_done,
+	     irq_on_packet,
+	     irq_end_of_packet,
+	     irq_end_of_calibration,
+	     irq_fifo_threshold,adc_on,adc_off:bool)
+    returns (a_on,red:bool)
+
+contract
+    enforce (not (a_on & red)) with (ok_r,ok_a:bool)
+
+let
+  a_on = inlined adc(adc_on,adc_off,ok_a);
+  red = inlined transceiver(enter_tx,
+			    enter_rx,
+			    exit_rx,
+			    calibrate,
+			    sleep,
+			    wake_up,
+			    irq_tx_done,
+			    irq_on_packet,
+			    irq_end_of_packet,
+			    irq_end_of_calibration,
+			    irq_fifo_threshold,ok_r);
+tel
+
+node period<<n,ini:int>>() = (s:bool)
+var c:int;
+let
+  c = ini fby (if s then 1 else c + 1);
+  s = c = n;
+tel
+
+    
+(* CHECK main *)
+node main() returns (ok:bool)
+var enter_tx,
+  enter_rx,
+  exit_rx,
+  calibrate,
+  sleep,
+  wake_up,
+  irq_tx_done,
+  irq_on_packet,
+  irq_end_of_packet,
+  irq_end_of_calibration,
+  irq_fifo_threshold,adc_on,adc_off:bool;
+  a_on,red:bool;
+let
+  (a_on,red) = main_rt(enter_tx,
+	                 enter_rx,
+	                 exit_rx,
+	                 calibrate,
+	                 sleep,
+	                 wake_up,
+	                 irq_tx_done,
+	                 irq_on_packet,
+	                 irq_end_of_packet,
+	                 irq_end_of_calibration,
+	                 irq_fifo_threshold,adc_on,adc_off);
+  ok = not (a_on & red);
+  enter_tx = period<<27,25>>();
+  enter_rx = period<<27,9>>();
+  exit_rx = period<<27,1>>();
+  calibrate = period<<27,19>>();
+  sleep = period<<27,14>>();
+  wake_up = period<<27,11>>();
+  irq_tx_done = period<<27,21>>();
+  irq_on_packet = period<<27,8>>();
+  irq_end_of_packet = period<<27,4>>();
+  irq_end_of_calibration = period<<27,16>>();
+  irq_fifo_threshold = period<<27,3>>();
+  adc_on = period<<17,13>>();
+  adc_off = period<<17,4>>();
+tel
diff --git a/test/sdc/servers.ept b/test/sdc/servers.ept
new file mode 100644
index 0000000..8502544
--- /dev/null
+++ b/test/sdc/servers.ept
@@ -0,0 +1,43 @@
+type mode = H | M | L
+
+node server(max:int) = (load:int)
+  contract
+  assume (max >= 5)
+  enforce (load <= max)
+  with (c:mode)
+let
+  switch c
+  | H do load = 20
+  | M do load = 10
+  | L do load = 0
+  end
+tel
+
+type degmode = Normal | Degraded
+  
+node degraded_server(max:int) = (load:int)
+  contract
+  assume (max >= 10)
+  enforce (load <= max)
+with (cm:mode;cd:degmode)
+let
+    switch cd
+    | Normal do
+        switch cm
+        | H do load = 20
+        | M do load = 10
+        | L do load = 0
+        end
+    | Degraded do load = 2
+    end
+tel
+
+(* CHECK main *)
+node main() = (ok:bool)
+  var max, load1, load2 : int;
+let
+    load1 = 0;
+  load2 = degraded_server(max);
+  max = 10;
+  ok = (load1 <= max) & (load2 <= max);
+tel
diff --git a/test/sdc/tracking.ept b/test/sdc/tracking.ept
index 0bbf147..dfcbc9d 100644
--- a/test/sdc/tracking.ept
+++ b/test/sdc/tracking.ept
@@ -111,7 +111,21 @@ let
 tel 
 
 
-
+(* CHECK main *)
+node main() = (ok:bool)
+var i_objvt, i_deadline, i_indice :level; s, e : bool;
+  objectives:bool; st_objvt, st_deadline, st_indice :level; res: int; wEx: elevel; win : wSize; running : bool;
+  l : int;
+let
+  (objectives,st_objvt,st_deadline,st_indice,res,wEx,win,running) = tracking(i_objvt,i_deadline,i_indice,s,e);
+  i_objvt = None fby None fby High fby None fby Bad fby None fby None fby Low fby None fby Low fby None fby Normal fby None fby i_objvt;
+  i_deadline = None fby Normal fby None fby None fby Normal fby None fby High fby None fby Low fby None fby None fby Bad fby None fby None fby None fby High fby None fby i_deadline;
+  i_indice = None fby None fby None fby Normal fby High fby Low fby None fby None fby Bad fby Bad fby None fby i_indice;
+  l = 0 fby (if l = 17 then 0 else l + 1);
+  s = (l = 7);
+  e = (l = 17);
+  ok = objectives;
+tel
 
 (*