From 62c20824dfd6b3b3a6f171e11e8b7c2125850b21 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Thu, 9 Dec 2021 14:20:41 +0100
Subject: [PATCH] add k annotations for k-induction in contracts
---
offline_tests/DRAGON_1.lus | 2 +-
offline_tests/DRAGON_10.lus | 2 +-
offline_tests/DRAGON_10_e1_3587_e3_2749.lus | 2 +-
offline_tests/DRAGON_10_e1_998.lus | 2 +-
offline_tests/DRAGON_10_e2_2785_e3_1744.lus | 2 +-
offline_tests/DRAGON_10_e2_402.lus | 2 +-
offline_tests/DRAGON_10_e3_144_e5_2046.lus | 2 +-
offline_tests/DRAGON_10_e3_3429.lus | 2 +-
offline_tests/DRAGON_1_e1_5070.lus | 2 +-
offline_tests/DRAGON_1_e2_1997.lus | 2 +-
offline_tests/DRAGON_2.lus | 2 +-
offline_tests/DRAGON_2_e1_2316.lus | 2 +-
offline_tests/DRAGON_2_e2_3183_e1_2644.lus | 2 +-
offline_tests/DRAGON_2_e2_3183_e2_3580.lus | 2 +-
offline_tests/DRAGON_2_e2_3183_e3_5972.lus | 2 +-
offline_tests/DRAGON_2_e2_4481.lus | 2 +-
offline_tests/DRAGON_2_e7_25_e8_3171.lus | 2 +-
offline_tests/DRAGON_3.lus | 2 +-
offline_tests/DRAGON_3_e1_4783.lus | 2 +-
offline_tests/DRAGON_3_e1_4783_e1_3755.lus | 2 +-
offline_tests/DRAGON_3_e1_4783_e2_158.lus | 2 +-
offline_tests/DRAGON_3_e1_4783_e3_511.lus | 2 +-
offline_tests/DRAGON_3_e2_5343_e1_988.lus | 2 +-
offline_tests/DRAGON_3_e3_3846.lus | 2 +-
offline_tests/DRAGON_3_e3_5422_e1_2288.lus | 2 +-
offline_tests/DRAGON_3_e3_5422_e2_3135.lus | 2 +-
offline_tests/DRAGON_6.lus | 2 +-
offline_tests/DRAGON_7.lus | 2 +-
offline_tests/DRAGON_7_e2_2872_e2_5844.lus | 2 +-
offline_tests/DRAGON_7_e2_2872_e3_2640.lus | 2 +-
offline_tests/DRAGON_9.lus | 2 +-
offline_tests/DRAGON_all.lus | 2 +-
offline_tests/DRAGON_all_e1_4022_e1_1759.lus | 2 +-
offline_tests/DRAGON_all_e1_4022_e2_267.lus | 2 +-
offline_tests/DRAGON_all_e1_4022_e3_3628.lus | 2 +-
offline_tests/DRAGON_all_e1_4037.lus | 2 +-
offline_tests/DRAGON_all_e2_6104.lus | 2 +-
offline_tests/DRAGON_all_e2_6104_e1_6205.lus | 2 +-
offline_tests/DRAGON_all_e2_6104_e2_3308.lus | 2 +-
offline_tests/DRAGON_all_e2_6104_e3_2607.lus | 2 +-
offline_tests/DRAGON_all_e3_4821_e1_1318.lus | 2 +-
offline_tests/DRAGON_all_e3_4821_e2_1089.lus | 2 +-
offline_tests/DRAGON_all_e3_4821_e4_1791.lus | 2 +-
offline_tests/DRAGON_all_e3_4821_e5_1536.lus | 2 +-
offline_tests/DRAGON_all_e3_5957.lus | 2 +-
offline_tests/FIREFLY_1.lus | 2 +-
offline_tests/FIREFLY_10.lus | 2 +-
offline_tests/FIREFLY_1_e1_1092_e2_1853.lus | 2 +-
offline_tests/FIREFLY_2.lus | 2 +-
offline_tests/FIREFLY_3.lus | 2 +-
offline_tests/FIREFLY_3_e2_2236.lus | 2 +-
offline_tests/FIREFLY_3_e2_2236_e1_2305.lus | 2 +-
offline_tests/FIREFLY_3_e2_2236_e2_1058.lus | 2 +-
offline_tests/FIREFLY_4.lus | 2 +-
offline_tests/FIREFLY_5.lus | 2 +-
offline_tests/FIREFLY_5_e2_2229.lus | 2 +-
offline_tests/FIREFLY_5_e2_2884.lus | 2 +-
offline_tests/FIREFLY_5_e2_2884_e1_2678.lus | 2 +-
offline_tests/FIREFLY_5_e2_2884_e2_1492.lus | 2 +-
offline_tests/FIREFLY_5_e2_2884_e3_1882.lus | 2 +-
offline_tests/FIREFLY_8.lus | 2 +-
offline_tests/FIREFLY_8_e2_1711.lus | 2 +-
offline_tests/FIREFLY_8_e2_1711_e1_1489.lus | 2 +-
offline_tests/FIREFLY_8_e2_1711_e2_2673.lus | 2 +-
offline_tests/FIREFLY_8_e2_1711_e3_1753.lus | 2 +-
offline_tests/FIREFLY_9.lus | 2 +-
offline_tests/FIREFLY_a3.lus | 2 +-
offline_tests/FIREFLY_a3_e1_3233_e2_2392.lus | 2 +-
offline_tests/FIREFLY_a3_e1_3233_e3_2970.lus | 2 +-
offline_tests/FIREFLY_a3_e2_2086_e1_3235.lus | 2 +-
offline_tests/FIREFLY_a3_e2_2086_e2_2689.lus | 2 +-
offline_tests/FIREFLY_a3_e2_2086_e3_2542.lus | 2 +-
offline_tests/FIREFLY_a3_e2_2952.lus | 2 +-
offline_tests/FIREFLY_a3_e3_314_e2_2812.lus | 2 +-
offline_tests/FIREFLY_all.lus | 2 +-
offline_tests/FIREFLY_all_e1_1207_e2_3220.lus | 2 +-
offline_tests/FIREFLY_all_e2_2924_e1_768.lus | 2 +-
offline_tests/FIREFLY_luke_1b.lus | 2 +-
.../FIREFLY_luke_1b_e1_1139_e2_2893.lus | 2 +-
.../FIREFLY_luke_1b_e2_3049_e1_946.lus | 2 +-
.../FIREFLY_luke_1b_e3_671_e6_1974.lus | 2 +-
.../FIREFLY_luke_1b_e7_3191_e8_2830.lus | 2 +-
offline_tests/FIREFLY_luke_rt.lus | 2 +-
.../FIREFLY_luke_rt_e1_913_e2_3353.lus | 2 +-
.../FIREFLY_luke_rt_e2_3460_e1_1455.lus | 2 +-
offline_tests/ILLINOIS_1.lus | 2 +-
offline_tests/ILLINOIS_2.lus | 2 +-
offline_tests/ILLINOIS_2_e1_834_e2_3395.lus | 2 +-
offline_tests/ILLINOIS_2_e2_2367_e1_3182.lus | 2 +-
offline_tests/ILLINOIS_3.lus | 2 +-
offline_tests/ILLINOIS_4.lus | 2 +-
offline_tests/ILLINOIS_5.lus | 2 +-
offline_tests/ILLINOIS_all.lus | 2 +-
offline_tests/MESI_1.lus | 2 +-
offline_tests/MESI_2.lus | 2 +-
offline_tests/MESI_3.lus | 2 +-
offline_tests/MESI_3_e1_2517_e8_2163.lus | 2 +-
offline_tests/MESI_3_e2_819_e1_1145.lus | 2 +-
offline_tests/MESI_3_e2_819_e4_1595.lus | 2 +-
offline_tests/MESI_3_e2_819_e6_1459.lus | 2 +-
offline_tests/MESI_3_e3_2669.lus | 2 +-
offline_tests/MESI_4.lus | 2 +-
offline_tests/MESI_all.lus | 2 +-
offline_tests/MOESI_1.lus | 2 +-
offline_tests/MOESI_2.lus | 2 +-
offline_tests/MOESI_2_e1_1753.lus | 2 +-
offline_tests/MOESI_2_e2_155.lus | 2 +-
offline_tests/MOESI_2_e2_1599.lus | 2 +-
offline_tests/MOESI_2_e2_1599_e8_1334.lus | 2 +-
offline_tests/MOESI_2_e3_1523.lus | 2 +-
offline_tests/MOESI_2_e3_929.lus | 2 +-
offline_tests/MOESI_2_e3_929_e4_578.lus | 2 +-
offline_tests/MOESI_2_e3_929_e5_1826.lus | 2 +-
offline_tests/MOESI_2_e3_929_e6_2707.lus | 2 +-
offline_tests/MOESI_2_e3_929_e8_1167.lus | 2 +-
offline_tests/MOESI_2_e7_2910_e8_2590.lus | 2 +-
offline_tests/MOESI_2_e8_101.lus | 2 +-
offline_tests/MOESI_2_e8_926.lus | 2 +-
offline_tests/MOESI_2_e8_926_e1_1065.lus | 2 +-
offline_tests/MOESI_2_e8_926_e2_349.lus | 2 +-
offline_tests/MOESI_2_e8_926_e3_1758.lus | 2 +-
offline_tests/MOESI_2_e8_926_e8_2138.lus | 2 +-
offline_tests/MOESI_all.lus | 2 +-
offline_tests/PRODUCER_CONSUMER_1.lus | 2 +-
offline_tests/PRODUCER_CONSUMER_2.lus | 2 +-
offline_tests/PRODUCER_CONSUMER_3.lus | 2 +-
offline_tests/PRODUCER_CONSUMER_all.lus | 2 +-
offline_tests/SYNAPSE_1.lus | 2 +-
offline_tests/SYNAPSE_123.lus | 2 +-
offline_tests/SYNAPSE_123_e8_953.lus | 2 +-
offline_tests/SYNAPSE_123_e8_953_e8_941.lus | 2 +-
offline_tests/SYNAPSE_2.lus | 2 +-
offline_tests/SYNAPSE_2_e8_1118_e7_1043.lus | 2 +-
offline_tests/SYNAPSE_2_e8_1118_e8_1177.lus | 2 +-
offline_tests/SYNAPSE_2_e8_656.lus | 2 +-
offline_tests/SYNAPSE_3.lus | 2 +-
offline_tests/SYNAPSE_3_e8_1329_e8_320.lus | 2 +-
offline_tests/SYNAPSE_3_e8_1708.lus | 2 +-
offline_tests/SYNAPSE_4.lus | 2 +-
offline_tests/SYNAPSE_4_e8_420_e7_572.lus | 2 +-
offline_tests/SYNAPSE_4_e8_420_e8_1525.lus | 2 +-
offline_tests/SYNAPSE_4_e8_974.lus | 2 +-
offline_tests/SYNAPSE_all.lus | 2 +-
offline_tests/SYNAPSE_all_e8_251.lus | 2 +-
offline_tests/_6counters_e8_371_e2_80.lus | 2 +-
offline_tests/car_1.lus | 2 +-
offline_tests/car_2.lus | 2 +-
offline_tests/car_3.lus | 2 +-
offline_tests/car_3_e2_695.lus | 2 +-
offline_tests/car_3_e2_777.lus | 2 +-
offline_tests/car_3_e7_626.lus | 2 +-
offline_tests/car_3_e8_33.lus | 2 +-
offline_tests/car_3_e8_33_e2_1010.lus | 2 +-
offline_tests/car_3_e8_33_e7_220.lus | 2 +-
offline_tests/car_4.lus | 2 +-
offline_tests/car_4_e3_57_e4_1047.lus | 2 +-
offline_tests/car_4_e3_57_e6_784.lus | 2 +-
offline_tests/car_4_e7_592.lus | 2 +-
offline_tests/car_4_e8_118.lus | 2 +-
offline_tests/car_all.lus | 2 +-
offline_tests/car_all_e2_142.lus | 2 +-
offline_tests/car_all_e3_1068_e4_275.lus | 2 +-
offline_tests/car_all_e8_856.lus | 2 +-
offline_tests/car_all_e8_856_e2_585.lus | 2 +-
offline_tests/ccp02.lus | 2 +-
offline_tests/ccp03.lus | 2 +-
offline_tests/ccp04.lus | 2 +-
offline_tests/ccp05.lus | 2 +-
offline_tests/ccp06.lus | 2 +-
offline_tests/ccp07.lus | 2 +-
offline_tests/ccp09.lus | 2 +-
offline_tests/ccp15.lus | 2 +-
offline_tests/ccp16.lus | 2 +-
offline_tests/ccp19.lus | 2 +-
offline_tests/cd.lus | 2 +-
offline_tests/counters.lus | 2 +-
offline_tests/cruise_controller_01.lus | 2 +-
offline_tests/cruise_controller_02.lus | 2 +-
offline_tests/cruise_controller_03.lus | 2 +-
offline_tests/cruise_controller_04.lus | 2 +-
offline_tests/cruise_controller_05.lus | 2 +-
offline_tests/cruise_controller_06.lus | 2 +-
offline_tests/cruise_controller_07.lus | 2 +-
offline_tests/cruise_controller_11.lus | 2 +-
offline_tests/cruise_controller_13.lus | 2 +-
offline_tests/durationThm_1_e2_3.lus | 2 +-
offline_tests/durationThm_1_e3_389_e4_294.lus | 2 +-
offline_tests/durationThm_1_e7_217_e2_352.lus | 2 +-
offline_tests/durationThm_2_e2_63.lus | 2 +-
offline_tests/durationThm_2_e3_329_e4_1.lus | 2 +-
offline_tests/durationThm_2_e7_145_e2_169.lus | 2 +-
offline_tests/durationThm_3_e2_148.lus | 2 +-
offline_tests/durationThm_3_e2_63.lus | 2 +-
offline_tests/durationThm_3_e3_207.lus | 2 +-
offline_tests/durationThm_3_e3_442.lus | 2 +-
offline_tests/durationThm_3_e3_442_e4_165.lus | 2 +-
offline_tests/durationThm_3_e3_442_e5_260.lus | 2 +-
offline_tests/durationThm_3_e7_334_e2_62.lus | 2 +-
offline_tests/ex3_e7_590_e7_590.lus | 2 +-
offline_tests/ex3_e7_655.lus | 2 +-
offline_tests/ex3_e8_381.lus | 2 +-
offline_tests/ex3_e8_381_e7_224.lus | 2 +-
offline_tests/ex3_e8_381_e8_477.lus | 2 +-
offline_tests/fast_1.lus | 2 +-
offline_tests/fast_1_e8_747_e8_1041.lus | 2 +-
offline_tests/fast_1_e8_751.lus | 2 +-
offline_tests/fast_2.lus | 2 +-
offline_tests/fast_2_e8_460_e8_1920.lus | 2 +-
offline_tests/fast_2_e8_976.lus | 2 +-
offline_tests/heater4.lus | 4 +-
offline_tests/hysteresis_1.lus | 2 +-
offline_tests/hysteresis_2.lus | 2 +-
offline_tests/hysteresis_3.lus | 2 +-
offline_tests/hysteresis_all.lus | 2 +-
offline_tests/ignored | 982 +++++++++++++-----
offline_tests/metros_1.lus | 2 +-
offline_tests/metros_1_e1_846_e1_1317.lus | 2 +-
offline_tests/metros_1_e1_846_e2_1394.lus | 2 +-
offline_tests/metros_1_e1_846_e3_1060.lus | 2 +-
offline_tests/metros_1_e1_846_e7_397.lus | 2 +-
offline_tests/metros_1_e2_1102_e1_317.lus | 2 +-
offline_tests/metros_1_e2_1102_e2_943.lus | 2 +-
offline_tests/metros_1_e2_1102_e3_961.lus | 2 +-
offline_tests/metros_1_e2_1102_e7_1163.lus | 2 +-
offline_tests/metros_1_e2_627.lus | 2 +-
offline_tests/metros_1_e7_1255_e7_12.lus | 2 +-
offline_tests/metros_1_e7_606.lus | 2 +-
offline_tests/metros_1_e8_725.lus | 2 +-
offline_tests/metros_1_e8_725_e1_919.lus | 2 +-
offline_tests/metros_1_e8_725_e2_1144.lus | 2 +-
offline_tests/metros_1_e8_725_e3_556.lus | 2 +-
offline_tests/metros_2_e1_1116_e2_617.lus | 2 +-
offline_tests/metros_2_e2_704_e2_13.lus | 2 +-
offline_tests/metros_3_e3_1275_e2_454.lus | 2 +-
offline_tests/metros_3_e3_1275_e3_640.lus | 2 +-
offline_tests/metros_4_e2_968_e2_1166.lus | 2 +-
offline_tests/metros_4_e2_968_e3_931.lus | 2 +-
offline_tests/metros_4_e3_1091_e2_1317.lus | 2 +-
offline_tests/metros_4_e3_1091_e3_522.lus | 2 +-
offline_tests/microwave01.lus | 2 +-
offline_tests/microwave02.lus | 2 +-
offline_tests/microwave03.lus | 2 +-
offline_tests/microwave04.lus | 2 +-
offline_tests/microwave05.lus | 2 +-
offline_tests/microwave15.lus | 2 +-
offline_tests/microwave16.lus | 2 +-
offline_tests/peterson_1.lus | 2 +-
offline_tests/peterson_2.lus | 2 +-
offline_tests/peterson_3.lus | 2 +-
offline_tests/peterson_4.lus | 2 +-
offline_tests/peterson_all.lus | 2 +-
offline_tests/readwrit.lus | 2 +-
offline_tests/rtp_1.lus | 2 +-
offline_tests/rtp_10.lus | 2 +-
offline_tests/rtp_2.lus | 2 +-
offline_tests/rtp_3.lus | 2 +-
offline_tests/rtp_4.lus | 2 +-
offline_tests/rtp_5.lus | 2 +-
offline_tests/rtp_6.lus | 2 +-
offline_tests/rtp_7.lus | 2 +-
offline_tests/rtp_8.lus | 2 +-
offline_tests/rtp_9.lus | 2 +-
offline_tests/rtp_all.lus | 2 +-
offline_tests/speed2.lus | 2 +-
offline_tests/speed2_e7_223_e7_213.lus | 2 +-
offline_tests/speed2_e7_223_e8_329.lus | 2 +-
offline_tests/speed2_e7_496.lus | 2 +-
offline_tests/speed2_e8_449.lus | 2 +-
offline_tests/speed2_e8_449_e7_353.lus | 2 +-
offline_tests/speed2_e8_449_e8_517.lus | 2 +-
offline_tests/speed2_e8_750.lus | 2 +-
offline_tests/speed_e7_207.lus | 2 +-
offline_tests/speed_e7_207_e7_538.lus | 2 +-
offline_tests/speed_e7_207_e8_507.lus | 2 +-
offline_tests/speed_e7_492.lus | 2 +-
offline_tests/speed_e8_649.lus | 2 +-
offline_tests/speed_e8_649_e7_709.lus | 2 +-
offline_tests/stalmark.lus | 2 +-
offline_tests/stalmark_e7_27.lus | 2 +-
offline_tests/stalmark_e7_27_e7_31.lus | 2 +-
offline_tests/stalmark_e7_76.lus | 2 +-
.../steam_boiler_no_arr2_e6_3003_e4_15091.lus | 2 +-
offline_tests/switch.lus | 22 +-
offline_tests/switch2.lus | 22 +-
offline_tests/test.ml | 9 +-
offline_tests/ticket3i_1.lus | 2 +-
offline_tests/ticket3i_2.lus | 2 +-
offline_tests/ticket3i_3.lus | 2 +-
offline_tests/ticket3i_3_e7_1312_e8_1916.lus | 2 +-
offline_tests/ticket3i_3_e8_1703.lus | 2 +-
offline_tests/ticket3i_3_e8_1703_e8_2560.lus | 2 +-
offline_tests/ticket3i_3_e8_1788.lus | 2 +-
offline_tests/ticket3i_4.lus | 2 +-
offline_tests/ticket3i_5.lus | 2 +-
offline_tests/ticket3i_6.lus | 2 +-
offline_tests/ticket3i_7_e1_2192_e1_1852.lus | 2 +-
offline_tests/ticket3i_all.lus | 2 +-
offline_tests/traffic.lus | 2 +-
offline_tests/tramway.lus | 2 +-
offline_tests/tramway_e7_1834.lus | 2 +-
offline_tests/tramway_e7_1834_e7_2363.lus | 2 +-
offline_tests/tramway_e7_1834_e8_3192.lus | 2 +-
offline_tests/tramway_e7_3304.lus | 2 +-
offline_tests/two_counters.lus | 2 +-
offline_tests/ums.lus | 2 +-
offline_tests/ums_e8_1032.lus | 2 +-
src/backends/C/c_backend_spec.ml | 22 +-
307 files changed, 1045 insertions(+), 618 deletions(-)
diff --git a/offline_tests/DRAGON_1.lus b/offline_tests/DRAGON_1.lus
index 42ebe80b..9eca443b 100644
--- a/offline_tests/DRAGON_1.lus
+++ b/offline_tests/DRAGON_1.lus
@@ -94,7 +94,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
let
diff --git a/offline_tests/DRAGON_10.lus b/offline_tests/DRAGON_10.lus
index 89106475..3a5d625c 100644
--- a/offline_tests/DRAGON_10.lus
+++ b/offline_tests/DRAGON_10.lus
@@ -95,7 +95,7 @@ tel
-- Not provable with luke-bitvec
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_10_e1_3587_e3_2749.lus b/offline_tests/DRAGON_10_e1_3587_e3_2749.lus
index 2b4710ae..98e56420 100644
--- a/offline_tests/DRAGON_10_e1_3587_e3_2749.lus
+++ b/offline_tests/DRAGON_10_e1_3587_e3_2749.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_10_e1_998.lus b/offline_tests/DRAGON_10_e1_998.lus
index cedd86b2..4f656dd1 100644
--- a/offline_tests/DRAGON_10_e1_998.lus
+++ b/offline_tests/DRAGON_10_e1_998.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_10_e2_2785_e3_1744.lus b/offline_tests/DRAGON_10_e2_2785_e3_1744.lus
index 448bdf45..ea84210b 100644
--- a/offline_tests/DRAGON_10_e2_2785_e3_1744.lus
+++ b/offline_tests/DRAGON_10_e2_2785_e3_1744.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_10_e2_402.lus b/offline_tests/DRAGON_10_e2_402.lus
index 5d4db224..b93e428d 100644
--- a/offline_tests/DRAGON_10_e2_402.lus
+++ b/offline_tests/DRAGON_10_e2_402.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_10_e3_144_e5_2046.lus b/offline_tests/DRAGON_10_e3_144_e5_2046.lus
index 31cec036..f423cfcb 100644
--- a/offline_tests/DRAGON_10_e3_144_e5_2046.lus
+++ b/offline_tests/DRAGON_10_e3_144_e5_2046.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_10_e3_3429.lus b/offline_tests/DRAGON_10_e3_3429.lus
index f53af9fc..5f48ee43 100644
--- a/offline_tests/DRAGON_10_e3_3429.lus
+++ b/offline_tests/DRAGON_10_e3_3429.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_1_e1_5070.lus b/offline_tests/DRAGON_1_e1_5070.lus
index 466636e1..7670834c 100644
--- a/offline_tests/DRAGON_1_e1_5070.lus
+++ b/offline_tests/DRAGON_1_e1_5070.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
let
diff --git a/offline_tests/DRAGON_1_e2_1997.lus b/offline_tests/DRAGON_1_e2_1997.lus
index d91e6cf1..175b69ed 100644
--- a/offline_tests/DRAGON_1_e2_1997.lus
+++ b/offline_tests/DRAGON_1_e2_1997.lus
@@ -82,7 +82,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
let
diff --git a/offline_tests/DRAGON_2.lus b/offline_tests/DRAGON_2.lus
index 56f22c53..dbf20fbd 100644
--- a/offline_tests/DRAGON_2.lus
+++ b/offline_tests/DRAGON_2.lus
@@ -94,7 +94,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_2_e1_2316.lus b/offline_tests/DRAGON_2_e1_2316.lus
index 0216eb2b..511cea81 100644
--- a/offline_tests/DRAGON_2_e1_2316.lus
+++ b/offline_tests/DRAGON_2_e1_2316.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_2_e2_3183_e1_2644.lus b/offline_tests/DRAGON_2_e2_3183_e1_2644.lus
index 1d523cf5..3d5402e1 100644
--- a/offline_tests/DRAGON_2_e2_3183_e1_2644.lus
+++ b/offline_tests/DRAGON_2_e2_3183_e1_2644.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_2_e2_3183_e2_3580.lus b/offline_tests/DRAGON_2_e2_3183_e2_3580.lus
index f8e39ae5..7c3c611b 100644
--- a/offline_tests/DRAGON_2_e2_3183_e2_3580.lus
+++ b/offline_tests/DRAGON_2_e2_3183_e2_3580.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_2_e2_3183_e3_5972.lus b/offline_tests/DRAGON_2_e2_3183_e3_5972.lus
index b872109f..b124e5aa 100644
--- a/offline_tests/DRAGON_2_e2_3183_e3_5972.lus
+++ b/offline_tests/DRAGON_2_e2_3183_e3_5972.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_2_e2_4481.lus b/offline_tests/DRAGON_2_e2_4481.lus
index 1909322b..7d1042e7 100644
--- a/offline_tests/DRAGON_2_e2_4481.lus
+++ b/offline_tests/DRAGON_2_e2_4481.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_2_e7_25_e8_3171.lus b/offline_tests/DRAGON_2_e7_25_e8_3171.lus
index f8bdbede..f59ceb1b 100644
--- a/offline_tests/DRAGON_2_e7_25_e8_3171.lus
+++ b/offline_tests/DRAGON_2_e7_25_e8_3171.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_3.lus b/offline_tests/DRAGON_3.lus
index 5927c29a..05973d13 100644
--- a/offline_tests/DRAGON_3.lus
+++ b/offline_tests/DRAGON_3.lus
@@ -102,7 +102,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_3_e1_4783.lus b/offline_tests/DRAGON_3_e1_4783.lus
index b1db6758..f5358d9d 100644
--- a/offline_tests/DRAGON_3_e1_4783.lus
+++ b/offline_tests/DRAGON_3_e1_4783.lus
@@ -87,7 +87,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_3_e1_4783_e1_3755.lus b/offline_tests/DRAGON_3_e1_4783_e1_3755.lus
index 7a666ccf..4c23b900 100644
--- a/offline_tests/DRAGON_3_e1_4783_e1_3755.lus
+++ b/offline_tests/DRAGON_3_e1_4783_e1_3755.lus
@@ -87,7 +87,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_3_e1_4783_e2_158.lus b/offline_tests/DRAGON_3_e1_4783_e2_158.lus
index b636f732..a5314027 100644
--- a/offline_tests/DRAGON_3_e1_4783_e2_158.lus
+++ b/offline_tests/DRAGON_3_e1_4783_e2_158.lus
@@ -87,7 +87,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_3_e1_4783_e3_511.lus b/offline_tests/DRAGON_3_e1_4783_e3_511.lus
index 9827b465..029f4422 100644
--- a/offline_tests/DRAGON_3_e1_4783_e3_511.lus
+++ b/offline_tests/DRAGON_3_e1_4783_e3_511.lus
@@ -87,7 +87,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_3_e2_5343_e1_988.lus b/offline_tests/DRAGON_3_e2_5343_e1_988.lus
index ddea8c12..2dd1c5e6 100644
--- a/offline_tests/DRAGON_3_e2_5343_e1_988.lus
+++ b/offline_tests/DRAGON_3_e2_5343_e1_988.lus
@@ -87,7 +87,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_3_e3_3846.lus b/offline_tests/DRAGON_3_e3_3846.lus
index c265ee17..c24841a6 100644
--- a/offline_tests/DRAGON_3_e3_3846.lus
+++ b/offline_tests/DRAGON_3_e3_3846.lus
@@ -87,7 +87,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_3_e3_5422_e1_2288.lus b/offline_tests/DRAGON_3_e3_5422_e1_2288.lus
index 226e2e76..10fd8825 100644
--- a/offline_tests/DRAGON_3_e3_5422_e1_2288.lus
+++ b/offline_tests/DRAGON_3_e3_5422_e1_2288.lus
@@ -87,7 +87,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_3_e3_5422_e2_3135.lus b/offline_tests/DRAGON_3_e3_5422_e2_3135.lus
index e7cee1bb..5e9428a0 100644
--- a/offline_tests/DRAGON_3_e3_5422_e2_3135.lus
+++ b/offline_tests/DRAGON_3_e3_5422_e2_3135.lus
@@ -87,7 +87,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_6.lus b/offline_tests/DRAGON_6.lus
index 2cd5978a..ff8e404b 100644
--- a/offline_tests/DRAGON_6.lus
+++ b/offline_tests/DRAGON_6.lus
@@ -94,7 +94,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_7.lus b/offline_tests/DRAGON_7.lus
index f5aba556..dcdd3f5e 100644
--- a/offline_tests/DRAGON_7.lus
+++ b/offline_tests/DRAGON_7.lus
@@ -95,7 +95,7 @@ tel
-- Not provable with luke-bitvec
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_7_e2_2872_e2_5844.lus b/offline_tests/DRAGON_7_e2_2872_e2_5844.lus
index 072b3d28..44a20854 100644
--- a/offline_tests/DRAGON_7_e2_2872_e2_5844.lus
+++ b/offline_tests/DRAGON_7_e2_2872_e2_5844.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_7_e2_2872_e3_2640.lus b/offline_tests/DRAGON_7_e2_2872_e3_2640.lus
index 1bac970b..27c4fa98 100644
--- a/offline_tests/DRAGON_7_e2_2872_e3_2640.lus
+++ b/offline_tests/DRAGON_7_e2_2872_e3_2640.lus
@@ -83,7 +83,7 @@ let
tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_9.lus b/offline_tests/DRAGON_9.lus
index f0d31ea6..36ff872d 100644
--- a/offline_tests/DRAGON_9.lus
+++ b/offline_tests/DRAGON_9.lus
@@ -95,7 +95,7 @@ tel
-- Not provable with luke-bitvec
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_all.lus b/offline_tests/DRAGON_all.lus
index c4957848..eace68f4 100644
--- a/offline_tests/DRAGON_all.lus
+++ b/offline_tests/DRAGON_all.lus
@@ -103,7 +103,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_all_e1_4022_e1_1759.lus b/offline_tests/DRAGON_all_e1_4022_e1_1759.lus
index edcecd3f..9f75bcd8 100644
--- a/offline_tests/DRAGON_all_e1_4022_e1_1759.lus
+++ b/offline_tests/DRAGON_all_e1_4022_e1_1759.lus
@@ -88,7 +88,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_all_e1_4022_e2_267.lus b/offline_tests/DRAGON_all_e1_4022_e2_267.lus
index 479176aa..5025b27f 100644
--- a/offline_tests/DRAGON_all_e1_4022_e2_267.lus
+++ b/offline_tests/DRAGON_all_e1_4022_e2_267.lus
@@ -88,7 +88,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_all_e1_4022_e3_3628.lus b/offline_tests/DRAGON_all_e1_4022_e3_3628.lus
index 88451ee5..bd89765c 100644
--- a/offline_tests/DRAGON_all_e1_4022_e3_3628.lus
+++ b/offline_tests/DRAGON_all_e1_4022_e3_3628.lus
@@ -88,7 +88,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_all_e1_4037.lus b/offline_tests/DRAGON_all_e1_4037.lus
index 5cdd1ab0..cba703d5 100644
--- a/offline_tests/DRAGON_all_e1_4037.lus
+++ b/offline_tests/DRAGON_all_e1_4037.lus
@@ -88,7 +88,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_all_e2_6104.lus b/offline_tests/DRAGON_all_e2_6104.lus
index 1af9e87a..09fb573c 100644
--- a/offline_tests/DRAGON_all_e2_6104.lus
+++ b/offline_tests/DRAGON_all_e2_6104.lus
@@ -88,7 +88,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_all_e2_6104_e1_6205.lus b/offline_tests/DRAGON_all_e2_6104_e1_6205.lus
index 862513c4..732c6608 100644
--- a/offline_tests/DRAGON_all_e2_6104_e1_6205.lus
+++ b/offline_tests/DRAGON_all_e2_6104_e1_6205.lus
@@ -88,7 +88,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_all_e2_6104_e2_3308.lus b/offline_tests/DRAGON_all_e2_6104_e2_3308.lus
index 913649f9..b1583ee0 100644
--- a/offline_tests/DRAGON_all_e2_6104_e2_3308.lus
+++ b/offline_tests/DRAGON_all_e2_6104_e2_3308.lus
@@ -88,7 +88,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_all_e2_6104_e3_2607.lus b/offline_tests/DRAGON_all_e2_6104_e3_2607.lus
index e382d85c..d9203e6d 100644
--- a/offline_tests/DRAGON_all_e2_6104_e3_2607.lus
+++ b/offline_tests/DRAGON_all_e2_6104_e3_2607.lus
@@ -88,7 +88,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_all_e3_4821_e1_1318.lus b/offline_tests/DRAGON_all_e3_4821_e1_1318.lus
index 20f787e0..dddaf0fb 100644
--- a/offline_tests/DRAGON_all_e3_4821_e1_1318.lus
+++ b/offline_tests/DRAGON_all_e3_4821_e1_1318.lus
@@ -88,7 +88,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_all_e3_4821_e2_1089.lus b/offline_tests/DRAGON_all_e3_4821_e2_1089.lus
index 9d77bbf3..835e5865 100644
--- a/offline_tests/DRAGON_all_e3_4821_e2_1089.lus
+++ b/offline_tests/DRAGON_all_e3_4821_e2_1089.lus
@@ -88,7 +88,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_all_e3_4821_e4_1791.lus b/offline_tests/DRAGON_all_e3_4821_e4_1791.lus
index abe55e7b..9dcd1c0c 100644
--- a/offline_tests/DRAGON_all_e3_4821_e4_1791.lus
+++ b/offline_tests/DRAGON_all_e3_4821_e4_1791.lus
@@ -88,7 +88,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_all_e3_4821_e5_1536.lus b/offline_tests/DRAGON_all_e3_4821_e5_1536.lus
index 8b7230db..4dc048d3 100644
--- a/offline_tests/DRAGON_all_e3_4821_e5_1536.lus
+++ b/offline_tests/DRAGON_all_e3_4821_e5_1536.lus
@@ -88,7 +88,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/DRAGON_all_e3_5957.lus b/offline_tests/DRAGON_all_e3_5957.lus
index 7eac2360..08f4bbeb 100644
--- a/offline_tests/DRAGON_all_e3_5957.lus
+++ b/offline_tests/DRAGON_all_e3_5957.lus
@@ -88,7 +88,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
init_invalid : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var exclusive, shared, shared_dirty, dirty, invalid : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/FIREFLY_1.lus b/offline_tests/FIREFLY_1.lus
index bd939ced..1b1d6588 100644
--- a/offline_tests/FIREFLY_1.lus
+++ b/offline_tests/FIREFLY_1.lus
@@ -74,7 +74,7 @@ tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_10.lus b/offline_tests/FIREFLY_10.lus
index 18cb3c1b..32b524d8 100644
--- a/offline_tests/FIREFLY_10.lus
+++ b/offline_tests/FIREFLY_10.lus
@@ -75,7 +75,7 @@ tel
-- Not provable in luke-bitvec
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_1_e1_1092_e2_1853.lus b/offline_tests/FIREFLY_1_e1_1092_e2_1853.lus
index ed84e7ec..54f6228a 100644
--- a/offline_tests/FIREFLY_1_e1_1092_e2_1853.lus
+++ b/offline_tests/FIREFLY_1_e1_1092_e2_1853.lus
@@ -61,7 +61,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_2.lus b/offline_tests/FIREFLY_2.lus
index 3b446311..bfa923eb 100644
--- a/offline_tests/FIREFLY_2.lus
+++ b/offline_tests/FIREFLY_2.lus
@@ -82,7 +82,7 @@ tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_3.lus b/offline_tests/FIREFLY_3.lus
index 7656b5fa..6f4d84e6 100644
--- a/offline_tests/FIREFLY_3.lus
+++ b/offline_tests/FIREFLY_3.lus
@@ -83,7 +83,7 @@ tel
-- Not provable in luke-bitvec
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_3_e2_2236.lus b/offline_tests/FIREFLY_3_e2_2236.lus
index 49b3f491..54cf49a2 100644
--- a/offline_tests/FIREFLY_3_e2_2236.lus
+++ b/offline_tests/FIREFLY_3_e2_2236.lus
@@ -65,7 +65,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_3_e2_2236_e1_2305.lus b/offline_tests/FIREFLY_3_e2_2236_e1_2305.lus
index e4863bc5..3dae3b0e 100644
--- a/offline_tests/FIREFLY_3_e2_2236_e1_2305.lus
+++ b/offline_tests/FIREFLY_3_e2_2236_e1_2305.lus
@@ -65,7 +65,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_3_e2_2236_e2_1058.lus b/offline_tests/FIREFLY_3_e2_2236_e2_1058.lus
index f1f97e22..58c31761 100644
--- a/offline_tests/FIREFLY_3_e2_2236_e2_1058.lus
+++ b/offline_tests/FIREFLY_3_e2_2236_e2_1058.lus
@@ -65,7 +65,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_4.lus b/offline_tests/FIREFLY_4.lus
index 5a67c87d..b60e4ba5 100644
--- a/offline_tests/FIREFLY_4.lus
+++ b/offline_tests/FIREFLY_4.lus
@@ -82,7 +82,7 @@ tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_5.lus b/offline_tests/FIREFLY_5.lus
index 15f23c71..e854b885 100644
--- a/offline_tests/FIREFLY_5.lus
+++ b/offline_tests/FIREFLY_5.lus
@@ -75,7 +75,7 @@ tel
-- Not provable in luke-bitvec
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_5_e2_2229.lus b/offline_tests/FIREFLY_5_e2_2229.lus
index cfe8ae48..9a307a7f 100644
--- a/offline_tests/FIREFLY_5_e2_2229.lus
+++ b/offline_tests/FIREFLY_5_e2_2229.lus
@@ -61,7 +61,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_5_e2_2884.lus b/offline_tests/FIREFLY_5_e2_2884.lus
index cfe8ae48..9a307a7f 100644
--- a/offline_tests/FIREFLY_5_e2_2884.lus
+++ b/offline_tests/FIREFLY_5_e2_2884.lus
@@ -61,7 +61,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_5_e2_2884_e1_2678.lus b/offline_tests/FIREFLY_5_e2_2884_e1_2678.lus
index 174277ce..2f1de3c5 100644
--- a/offline_tests/FIREFLY_5_e2_2884_e1_2678.lus
+++ b/offline_tests/FIREFLY_5_e2_2884_e1_2678.lus
@@ -61,7 +61,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_5_e2_2884_e2_1492.lus b/offline_tests/FIREFLY_5_e2_2884_e2_1492.lus
index 1187d845..d6a63e76 100644
--- a/offline_tests/FIREFLY_5_e2_2884_e2_1492.lus
+++ b/offline_tests/FIREFLY_5_e2_2884_e2_1492.lus
@@ -61,7 +61,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_5_e2_2884_e3_1882.lus b/offline_tests/FIREFLY_5_e2_2884_e3_1882.lus
index f5c18b70..259ce112 100644
--- a/offline_tests/FIREFLY_5_e2_2884_e3_1882.lus
+++ b/offline_tests/FIREFLY_5_e2_2884_e3_1882.lus
@@ -61,7 +61,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_8.lus b/offline_tests/FIREFLY_8.lus
index bfe828dc..1bf612ae 100644
--- a/offline_tests/FIREFLY_8.lus
+++ b/offline_tests/FIREFLY_8.lus
@@ -74,7 +74,7 @@ tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_8_e2_1711.lus b/offline_tests/FIREFLY_8_e2_1711.lus
index 83d24ef7..e40fe58e 100644
--- a/offline_tests/FIREFLY_8_e2_1711.lus
+++ b/offline_tests/FIREFLY_8_e2_1711.lus
@@ -61,7 +61,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_8_e2_1711_e1_1489.lus b/offline_tests/FIREFLY_8_e2_1711_e1_1489.lus
index 4e14db8c..cbd852e3 100644
--- a/offline_tests/FIREFLY_8_e2_1711_e1_1489.lus
+++ b/offline_tests/FIREFLY_8_e2_1711_e1_1489.lus
@@ -61,7 +61,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_8_e2_1711_e2_2673.lus b/offline_tests/FIREFLY_8_e2_1711_e2_2673.lus
index 43be3054..da4f57a9 100644
--- a/offline_tests/FIREFLY_8_e2_1711_e2_2673.lus
+++ b/offline_tests/FIREFLY_8_e2_1711_e2_2673.lus
@@ -61,7 +61,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_8_e2_1711_e3_1753.lus b/offline_tests/FIREFLY_8_e2_1711_e3_1753.lus
index 0d8759d4..d5a6332a 100644
--- a/offline_tests/FIREFLY_8_e2_1711_e3_1753.lus
+++ b/offline_tests/FIREFLY_8_e2_1711_e3_1753.lus
@@ -61,7 +61,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_9.lus b/offline_tests/FIREFLY_9.lus
index 922b470a..2c70da55 100644
--- a/offline_tests/FIREFLY_9.lus
+++ b/offline_tests/FIREFLY_9.lus
@@ -82,7 +82,7 @@ tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_a3.lus b/offline_tests/FIREFLY_a3.lus
index 075bbd76..b2989e34 100644
--- a/offline_tests/FIREFLY_a3.lus
+++ b/offline_tests/FIREFLY_a3.lus
@@ -82,7 +82,7 @@ tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
R4, A1, A2, A3 : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_a3_e1_3233_e2_2392.lus b/offline_tests/FIREFLY_a3_e1_3233_e2_2392.lus
index 19261f28..885bd8bb 100644
--- a/offline_tests/FIREFLY_a3_e1_3233_e2_2392.lus
+++ b/offline_tests/FIREFLY_a3_e1_3233_e2_2392.lus
@@ -65,7 +65,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
R4, A1, A2, A3 : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_a3_e1_3233_e3_2970.lus b/offline_tests/FIREFLY_a3_e1_3233_e3_2970.lus
index 906f371b..4713f8f7 100644
--- a/offline_tests/FIREFLY_a3_e1_3233_e3_2970.lus
+++ b/offline_tests/FIREFLY_a3_e1_3233_e3_2970.lus
@@ -65,7 +65,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
R4, A1, A2, A3 : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_a3_e2_2086_e1_3235.lus b/offline_tests/FIREFLY_a3_e2_2086_e1_3235.lus
index 46927ade..215db0a0 100644
--- a/offline_tests/FIREFLY_a3_e2_2086_e1_3235.lus
+++ b/offline_tests/FIREFLY_a3_e2_2086_e1_3235.lus
@@ -65,7 +65,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
R4, A1, A2, A3 : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_a3_e2_2086_e2_2689.lus b/offline_tests/FIREFLY_a3_e2_2086_e2_2689.lus
index 863abe15..22ea7851 100644
--- a/offline_tests/FIREFLY_a3_e2_2086_e2_2689.lus
+++ b/offline_tests/FIREFLY_a3_e2_2086_e2_2689.lus
@@ -65,7 +65,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
R4, A1, A2, A3 : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_a3_e2_2086_e3_2542.lus b/offline_tests/FIREFLY_a3_e2_2086_e3_2542.lus
index adb9d84c..264163f1 100644
--- a/offline_tests/FIREFLY_a3_e2_2086_e3_2542.lus
+++ b/offline_tests/FIREFLY_a3_e2_2086_e3_2542.lus
@@ -65,7 +65,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
R4, A1, A2, A3 : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_a3_e2_2952.lus b/offline_tests/FIREFLY_a3_e2_2952.lus
index 10608fc8..18d65e94 100644
--- a/offline_tests/FIREFLY_a3_e2_2952.lus
+++ b/offline_tests/FIREFLY_a3_e2_2952.lus
@@ -65,7 +65,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
R4, A1, A2, A3 : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_a3_e3_314_e2_2812.lus b/offline_tests/FIREFLY_a3_e3_314_e2_2812.lus
index 4422064d..6f1cc5ac 100644
--- a/offline_tests/FIREFLY_a3_e3_314_e2_2812.lus
+++ b/offline_tests/FIREFLY_a3_e3_314_e2_2812.lus
@@ -65,7 +65,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
R4, A1, A2, A3 : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_all.lus b/offline_tests/FIREFLY_all.lus
index e280dd7d..74bab4f8 100644
--- a/offline_tests/FIREFLY_all.lus
+++ b/offline_tests/FIREFLY_all.lus
@@ -82,7 +82,7 @@ tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_all_e1_1207_e2_3220.lus b/offline_tests/FIREFLY_all_e1_1207_e2_3220.lus
index 1d947a54..24057f2a 100644
--- a/offline_tests/FIREFLY_all_e1_1207_e2_3220.lus
+++ b/offline_tests/FIREFLY_all_e1_1207_e2_3220.lus
@@ -65,7 +65,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_all_e2_2924_e1_768.lus b/offline_tests/FIREFLY_all_e2_2924_e1_768.lus
index d8425493..b8038eb9 100644
--- a/offline_tests/FIREFLY_all_e2_2924_e1_768.lus
+++ b/offline_tests/FIREFLY_all_e2_2924_e1_768.lus
@@ -65,7 +65,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
procs : int;
diff --git a/offline_tests/FIREFLY_luke_1b.lus b/offline_tests/FIREFLY_luke_1b.lus
index 71fc0a5d..4b4f0f6e 100644
--- a/offline_tests/FIREFLY_luke_1b.lus
+++ b/offline_tests/FIREFLY_luke_1b.lus
@@ -77,7 +77,7 @@ tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_luke_1b_e1_1139_e2_2893.lus b/offline_tests/FIREFLY_luke_1b_e1_1139_e2_2893.lus
index aef254d6..a16e823b 100644
--- a/offline_tests/FIREFLY_luke_1b_e1_1139_e2_2893.lus
+++ b/offline_tests/FIREFLY_luke_1b_e1_1139_e2_2893.lus
@@ -61,7 +61,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_luke_1b_e2_3049_e1_946.lus b/offline_tests/FIREFLY_luke_1b_e2_3049_e1_946.lus
index 484221be..99964953 100644
--- a/offline_tests/FIREFLY_luke_1b_e2_3049_e1_946.lus
+++ b/offline_tests/FIREFLY_luke_1b_e2_3049_e1_946.lus
@@ -61,7 +61,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_luke_1b_e3_671_e6_1974.lus b/offline_tests/FIREFLY_luke_1b_e3_671_e6_1974.lus
index bb2bf3ba..030326ed 100644
--- a/offline_tests/FIREFLY_luke_1b_e3_671_e6_1974.lus
+++ b/offline_tests/FIREFLY_luke_1b_e3_671_e6_1974.lus
@@ -61,7 +61,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_luke_1b_e7_3191_e8_2830.lus b/offline_tests/FIREFLY_luke_1b_e7_3191_e8_2830.lus
index bb2bf3ba..030326ed 100644
--- a/offline_tests/FIREFLY_luke_1b_e7_3191_e8_2830.lus
+++ b/offline_tests/FIREFLY_luke_1b_e7_3191_e8_2830.lus
@@ -61,7 +61,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_luke_rt.lus b/offline_tests/FIREFLY_luke_rt.lus
index 1476497c..147cdda7 100644
--- a/offline_tests/FIREFLY_luke_rt.lus
+++ b/offline_tests/FIREFLY_luke_rt.lus
@@ -81,7 +81,7 @@ tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_luke_rt_e1_913_e2_3353.lus b/offline_tests/FIREFLY_luke_rt_e1_913_e2_3353.lus
index 17b18451..f5aa1a15 100644
--- a/offline_tests/FIREFLY_luke_rt_e1_913_e2_3353.lus
+++ b/offline_tests/FIREFLY_luke_rt_e1_913_e2_3353.lus
@@ -64,7 +64,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/FIREFLY_luke_rt_e2_3460_e1_1455.lus b/offline_tests/FIREFLY_luke_rt_e2_3460_e1_1455.lus
index c56c6f8f..5fb7577c 100644
--- a/offline_tests/FIREFLY_luke_rt_e2_3460_e1_1455.lus
+++ b/offline_tests/FIREFLY_luke_rt_e2_3460_e1_1455.lus
@@ -64,7 +64,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/ILLINOIS_1.lus b/offline_tests/ILLINOIS_1.lus
index 4b40938e..fccf963a 100644
--- a/offline_tests/ILLINOIS_1.lus
+++ b/offline_tests/ILLINOIS_1.lus
@@ -73,7 +73,7 @@ tel
node top(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int)
returns( OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/ILLINOIS_2.lus b/offline_tests/ILLINOIS_2.lus
index b5fcabf0..40ecc2da 100644
--- a/offline_tests/ILLINOIS_2.lus
+++ b/offline_tests/ILLINOIS_2.lus
@@ -73,7 +73,7 @@ tel
node top(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int)
returns( OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/ILLINOIS_2_e1_834_e2_3395.lus b/offline_tests/ILLINOIS_2_e1_834_e2_3395.lus
index 6549ace0..09e5a4cd 100644
--- a/offline_tests/ILLINOIS_2_e1_834_e2_3395.lus
+++ b/offline_tests/ILLINOIS_2_e1_834_e2_3395.lus
@@ -64,7 +64,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int)
returns( OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/ILLINOIS_2_e2_2367_e1_3182.lus b/offline_tests/ILLINOIS_2_e2_2367_e1_3182.lus
index 0643e786..bb940dcf 100644
--- a/offline_tests/ILLINOIS_2_e2_2367_e1_3182.lus
+++ b/offline_tests/ILLINOIS_2_e2_2367_e1_3182.lus
@@ -64,7 +64,7 @@ let
tel
node top(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int)
returns( OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/ILLINOIS_3.lus b/offline_tests/ILLINOIS_3.lus
index 28d58e7b..e689df9e 100644
--- a/offline_tests/ILLINOIS_3.lus
+++ b/offline_tests/ILLINOIS_3.lus
@@ -81,7 +81,7 @@ tel
node top(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int)
returns( OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/ILLINOIS_4.lus b/offline_tests/ILLINOIS_4.lus
index 5e82c228..31ccc974 100644
--- a/offline_tests/ILLINOIS_4.lus
+++ b/offline_tests/ILLINOIS_4.lus
@@ -74,7 +74,7 @@ tel
-- Not provable in luke-bitvec
node top(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int)
returns( OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/ILLINOIS_5.lus b/offline_tests/ILLINOIS_5.lus
index 923e84e4..d82d5ed8 100644
--- a/offline_tests/ILLINOIS_5.lus
+++ b/offline_tests/ILLINOIS_5.lus
@@ -73,7 +73,7 @@ tel
node top(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int)
returns( OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/ILLINOIS_all.lus b/offline_tests/ILLINOIS_all.lus
index 6d4bc58e..c2a893b1 100644
--- a/offline_tests/ILLINOIS_all.lus
+++ b/offline_tests/ILLINOIS_all.lus
@@ -81,7 +81,7 @@ tel
node top(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int)
returns( OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid, dirty, exclusive, shared : int;
env : bool;
let
diff --git a/offline_tests/MESI_1.lus b/offline_tests/MESI_1.lus
index d43afddb..cc85a37a 100644
--- a/offline_tests/MESI_1.lus
+++ b/offline_tests/MESI_1.lus
@@ -55,7 +55,7 @@ let
tel
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_me, exclusive_me, shared_me, invalid_me : int;
env : bool;
let
diff --git a/offline_tests/MESI_2.lus b/offline_tests/MESI_2.lus
index fe1f91f7..bfb903a8 100644
--- a/offline_tests/MESI_2.lus
+++ b/offline_tests/MESI_2.lus
@@ -55,7 +55,7 @@ let
tel
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_me, exclusive_me, shared_me, invalid_me : int;
env : bool;
let
diff --git a/offline_tests/MESI_3.lus b/offline_tests/MESI_3.lus
index 631718f6..f6405f41 100644
--- a/offline_tests/MESI_3.lus
+++ b/offline_tests/MESI_3.lus
@@ -61,7 +61,7 @@ tel
-- Only provable in nbac
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_me, exclusive_me, shared_me, invalid_me : int;
env : bool;
let
diff --git a/offline_tests/MESI_3_e1_2517_e8_2163.lus b/offline_tests/MESI_3_e1_2517_e8_2163.lus
index ce6a14da..43df9739 100644
--- a/offline_tests/MESI_3_e1_2517_e8_2163.lus
+++ b/offline_tests/MESI_3_e1_2517_e8_2163.lus
@@ -50,7 +50,7 @@ let
pre invalid_me;
tel
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_me, exclusive_me, shared_me, invalid_me : int;
env : bool;
let
diff --git a/offline_tests/MESI_3_e2_819_e1_1145.lus b/offline_tests/MESI_3_e2_819_e1_1145.lus
index 394323de..95852e6c 100644
--- a/offline_tests/MESI_3_e2_819_e1_1145.lus
+++ b/offline_tests/MESI_3_e2_819_e1_1145.lus
@@ -50,7 +50,7 @@ let
pre invalid_me;
tel
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_me, exclusive_me, shared_me, invalid_me : int;
env : bool;
let
diff --git a/offline_tests/MESI_3_e2_819_e4_1595.lus b/offline_tests/MESI_3_e2_819_e4_1595.lus
index 635c8783..f767daa6 100644
--- a/offline_tests/MESI_3_e2_819_e4_1595.lus
+++ b/offline_tests/MESI_3_e2_819_e4_1595.lus
@@ -50,7 +50,7 @@ let
pre invalid_me;
tel
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_me, exclusive_me, shared_me, invalid_me : int;
env : bool;
let
diff --git a/offline_tests/MESI_3_e2_819_e6_1459.lus b/offline_tests/MESI_3_e2_819_e6_1459.lus
index 468cc09c..678f84c0 100644
--- a/offline_tests/MESI_3_e2_819_e6_1459.lus
+++ b/offline_tests/MESI_3_e2_819_e6_1459.lus
@@ -50,7 +50,7 @@ let
pre invalid_me;
tel
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_me, exclusive_me, shared_me, invalid_me : int;
env : bool;
let
diff --git a/offline_tests/MESI_3_e3_2669.lus b/offline_tests/MESI_3_e3_2669.lus
index 937a7da5..618413d2 100644
--- a/offline_tests/MESI_3_e3_2669.lus
+++ b/offline_tests/MESI_3_e3_2669.lus
@@ -50,7 +50,7 @@ let
pre invalid_me;
tel
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_me, exclusive_me, shared_me, invalid_me : int;
env : bool;
let
diff --git a/offline_tests/MESI_4.lus b/offline_tests/MESI_4.lus
index f42ecc65..80bf9ea5 100644
--- a/offline_tests/MESI_4.lus
+++ b/offline_tests/MESI_4.lus
@@ -55,7 +55,7 @@ let
tel
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_me, exclusive_me, shared_me, invalid_me : int;
env : bool;
let
diff --git a/offline_tests/MESI_all.lus b/offline_tests/MESI_all.lus
index c05de509..0c2561cd 100644
--- a/offline_tests/MESI_all.lus
+++ b/offline_tests/MESI_all.lus
@@ -56,7 +56,7 @@ tel
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_me, exclusive_me, shared_me, invalid_me : int;
env : bool;
let
diff --git a/offline_tests/MOESI_1.lus b/offline_tests/MOESI_1.lus
index c1a567a1..7e5da704 100644
--- a/offline_tests/MOESI_1.lus
+++ b/offline_tests/MOESI_1.lus
@@ -62,7 +62,7 @@ tel
node top( init_invalid_mo : int;
etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
let
diff --git a/offline_tests/MOESI_2.lus b/offline_tests/MOESI_2.lus
index e6c252c5..614fb526 100644
--- a/offline_tests/MOESI_2.lus
+++ b/offline_tests/MOESI_2.lus
@@ -61,7 +61,7 @@ tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e1_1753.lus b/offline_tests/MOESI_2_e1_1753.lus
index 3533482a..b2490695 100644
--- a/offline_tests/MOESI_2_e1_1753.lus
+++ b/offline_tests/MOESI_2_e1_1753.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e2_155.lus b/offline_tests/MOESI_2_e2_155.lus
index e44090ab..c1ab3d7f 100644
--- a/offline_tests/MOESI_2_e2_155.lus
+++ b/offline_tests/MOESI_2_e2_155.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e2_1599.lus b/offline_tests/MOESI_2_e2_1599.lus
index e44090ab..c1ab3d7f 100644
--- a/offline_tests/MOESI_2_e2_1599.lus
+++ b/offline_tests/MOESI_2_e2_1599.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e2_1599_e8_1334.lus b/offline_tests/MOESI_2_e2_1599_e8_1334.lus
index 568cdc47..da8237d6 100644
--- a/offline_tests/MOESI_2_e2_1599_e8_1334.lus
+++ b/offline_tests/MOESI_2_e2_1599_e8_1334.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e3_1523.lus b/offline_tests/MOESI_2_e3_1523.lus
index a76d0801..3d89e013 100644
--- a/offline_tests/MOESI_2_e3_1523.lus
+++ b/offline_tests/MOESI_2_e3_1523.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e3_929.lus b/offline_tests/MOESI_2_e3_929.lus
index a76d0801..3d89e013 100644
--- a/offline_tests/MOESI_2_e3_929.lus
+++ b/offline_tests/MOESI_2_e3_929.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e3_929_e4_578.lus b/offline_tests/MOESI_2_e3_929_e4_578.lus
index e186f946..5dd3f792 100644
--- a/offline_tests/MOESI_2_e3_929_e4_578.lus
+++ b/offline_tests/MOESI_2_e3_929_e4_578.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e3_929_e5_1826.lus b/offline_tests/MOESI_2_e3_929_e5_1826.lus
index ca32ed1a..ede5e0f4 100644
--- a/offline_tests/MOESI_2_e3_929_e5_1826.lus
+++ b/offline_tests/MOESI_2_e3_929_e5_1826.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e3_929_e6_2707.lus b/offline_tests/MOESI_2_e3_929_e6_2707.lus
index c6555bfc..c596df46 100644
--- a/offline_tests/MOESI_2_e3_929_e6_2707.lus
+++ b/offline_tests/MOESI_2_e3_929_e6_2707.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e3_929_e8_1167.lus b/offline_tests/MOESI_2_e3_929_e8_1167.lus
index fb1e2055..5c4635ff 100644
--- a/offline_tests/MOESI_2_e3_929_e8_1167.lus
+++ b/offline_tests/MOESI_2_e3_929_e8_1167.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e7_2910_e8_2590.lus b/offline_tests/MOESI_2_e7_2910_e8_2590.lus
index c6555bfc..c596df46 100644
--- a/offline_tests/MOESI_2_e7_2910_e8_2590.lus
+++ b/offline_tests/MOESI_2_e7_2910_e8_2590.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e8_101.lus b/offline_tests/MOESI_2_e8_101.lus
index 8d20b92d..f6895a96 100644
--- a/offline_tests/MOESI_2_e8_101.lus
+++ b/offline_tests/MOESI_2_e8_101.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e8_926.lus b/offline_tests/MOESI_2_e8_926.lus
index 8d20b92d..f6895a96 100644
--- a/offline_tests/MOESI_2_e8_926.lus
+++ b/offline_tests/MOESI_2_e8_926.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e8_926_e1_1065.lus b/offline_tests/MOESI_2_e8_926_e1_1065.lus
index d3125beb..e156c050 100644
--- a/offline_tests/MOESI_2_e8_926_e1_1065.lus
+++ b/offline_tests/MOESI_2_e8_926_e1_1065.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e8_926_e2_349.lus b/offline_tests/MOESI_2_e8_926_e2_349.lus
index 568cdc47..da8237d6 100644
--- a/offline_tests/MOESI_2_e8_926_e2_349.lus
+++ b/offline_tests/MOESI_2_e8_926_e2_349.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e8_926_e3_1758.lus b/offline_tests/MOESI_2_e8_926_e3_1758.lus
index fb1e2055..5c4635ff 100644
--- a/offline_tests/MOESI_2_e8_926_e3_1758.lus
+++ b/offline_tests/MOESI_2_e8_926_e3_1758.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_2_e8_926_e8_2138.lus b/offline_tests/MOESI_2_e8_926_e8_2138.lus
index 4781b350..8a7df27c 100644
--- a/offline_tests/MOESI_2_e8_926_e8_2138.lus
+++ b/offline_tests/MOESI_2_e8_926_e8_2138.lus
@@ -50,7 +50,7 @@ let
tel
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/MOESI_all.lus b/offline_tests/MOESI_all.lus
index e1d26049..ae1abaaf 100644
--- a/offline_tests/MOESI_all.lus
+++ b/offline_tests/MOESI_all.lus
@@ -62,7 +62,7 @@ tel
node top( init_invalid_mo : int;
etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
erreur_mo : bool;
env : bool;
diff --git a/offline_tests/PRODUCER_CONSUMER_1.lus b/offline_tests/PRODUCER_CONSUMER_1.lus
index 3e6d2102..a38ec0a3 100644
--- a/offline_tests/PRODUCER_CONSUMER_1.lus
+++ b/offline_tests/PRODUCER_CONSUMER_1.lus
@@ -40,7 +40,7 @@ tel
-- Not provable with luke-bitvec
node top(etat1, etat2, etat3 : bool; a_init : int) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var i, b, a, o1, o2 : int;
env : bool;
let
diff --git a/offline_tests/PRODUCER_CONSUMER_2.lus b/offline_tests/PRODUCER_CONSUMER_2.lus
index f7297297..1adf15aa 100644
--- a/offline_tests/PRODUCER_CONSUMER_2.lus
+++ b/offline_tests/PRODUCER_CONSUMER_2.lus
@@ -39,7 +39,7 @@ let
tel
node top(etat1, etat2, etat3 : bool; a_init : int) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var i, b, a, o1, o2 : int;
env : bool;
let
diff --git a/offline_tests/PRODUCER_CONSUMER_3.lus b/offline_tests/PRODUCER_CONSUMER_3.lus
index 5ee072ad..c619b794 100644
--- a/offline_tests/PRODUCER_CONSUMER_3.lus
+++ b/offline_tests/PRODUCER_CONSUMER_3.lus
@@ -49,7 +49,7 @@ let
tel
node top(etat1, etat2, etat3 : bool; a_init : int) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var i, b, a, o1, o2 : int;
env : bool;
let
diff --git a/offline_tests/PRODUCER_CONSUMER_all.lus b/offline_tests/PRODUCER_CONSUMER_all.lus
index d05526e7..27a901a5 100644
--- a/offline_tests/PRODUCER_CONSUMER_all.lus
+++ b/offline_tests/PRODUCER_CONSUMER_all.lus
@@ -49,7 +49,7 @@ let
tel
node top(etat1, etat2, etat3 : bool; a_init : int) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var i, b, a, o1, o2 : int;
env : bool;
let
diff --git a/offline_tests/SYNAPSE_1.lus b/offline_tests/SYNAPSE_1.lus
index fc673e0b..7bc737ff 100644
--- a/offline_tests/SYNAPSE_1.lus
+++ b/offline_tests/SYNAPSE_1.lus
@@ -44,7 +44,7 @@ tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
env : bool;
let
diff --git a/offline_tests/SYNAPSE_123.lus b/offline_tests/SYNAPSE_123.lus
index 9de6067c..24357e42 100644
--- a/offline_tests/SYNAPSE_123.lus
+++ b/offline_tests/SYNAPSE_123.lus
@@ -49,7 +49,7 @@ tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
R1, R2, R3 : bool;
env : bool;
diff --git a/offline_tests/SYNAPSE_123_e8_953.lus b/offline_tests/SYNAPSE_123_e8_953.lus
index 4bbf3ed2..e0b9084d 100644
--- a/offline_tests/SYNAPSE_123_e8_953.lus
+++ b/offline_tests/SYNAPSE_123_e8_953.lus
@@ -37,7 +37,7 @@ let
tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
R1, R2, R3 : bool;
env : bool;
diff --git a/offline_tests/SYNAPSE_123_e8_953_e8_941.lus b/offline_tests/SYNAPSE_123_e8_953_e8_941.lus
index 89d0be60..0db434db 100644
--- a/offline_tests/SYNAPSE_123_e8_953_e8_941.lus
+++ b/offline_tests/SYNAPSE_123_e8_953_e8_941.lus
@@ -37,7 +37,7 @@ let
tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
R1, R2, R3 : bool;
env : bool;
diff --git a/offline_tests/SYNAPSE_2.lus b/offline_tests/SYNAPSE_2.lus
index 6cb24a14..21af8a45 100644
--- a/offline_tests/SYNAPSE_2.lus
+++ b/offline_tests/SYNAPSE_2.lus
@@ -44,7 +44,7 @@ tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
env : bool;
let
diff --git a/offline_tests/SYNAPSE_2_e8_1118_e7_1043.lus b/offline_tests/SYNAPSE_2_e8_1118_e7_1043.lus
index 84ae2878..c72d0d7a 100644
--- a/offline_tests/SYNAPSE_2_e8_1118_e7_1043.lus
+++ b/offline_tests/SYNAPSE_2_e8_1118_e7_1043.lus
@@ -34,7 +34,7 @@ let
tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
env : bool;
let
diff --git a/offline_tests/SYNAPSE_2_e8_1118_e8_1177.lus b/offline_tests/SYNAPSE_2_e8_1118_e8_1177.lus
index 76add05a..c1b97ec2 100644
--- a/offline_tests/SYNAPSE_2_e8_1118_e8_1177.lus
+++ b/offline_tests/SYNAPSE_2_e8_1118_e8_1177.lus
@@ -34,7 +34,7 @@ let
tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
env : bool;
let
diff --git a/offline_tests/SYNAPSE_2_e8_656.lus b/offline_tests/SYNAPSE_2_e8_656.lus
index cdb22969..2fc1a0f1 100644
--- a/offline_tests/SYNAPSE_2_e8_656.lus
+++ b/offline_tests/SYNAPSE_2_e8_656.lus
@@ -34,7 +34,7 @@ let
tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
env : bool;
let
diff --git a/offline_tests/SYNAPSE_3.lus b/offline_tests/SYNAPSE_3.lus
index 51559f07..3300c2d3 100644
--- a/offline_tests/SYNAPSE_3.lus
+++ b/offline_tests/SYNAPSE_3.lus
@@ -48,7 +48,7 @@ tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
env : bool;
let
diff --git a/offline_tests/SYNAPSE_3_e8_1329_e8_320.lus b/offline_tests/SYNAPSE_3_e8_1329_e8_320.lus
index 7d8173eb..fb7b0a9e 100644
--- a/offline_tests/SYNAPSE_3_e8_1329_e8_320.lus
+++ b/offline_tests/SYNAPSE_3_e8_1329_e8_320.lus
@@ -37,7 +37,7 @@ let
tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
env : bool;
let
diff --git a/offline_tests/SYNAPSE_3_e8_1708.lus b/offline_tests/SYNAPSE_3_e8_1708.lus
index c1a948a6..b717c8b4 100644
--- a/offline_tests/SYNAPSE_3_e8_1708.lus
+++ b/offline_tests/SYNAPSE_3_e8_1708.lus
@@ -37,7 +37,7 @@ let
tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
env : bool;
let
diff --git a/offline_tests/SYNAPSE_4.lus b/offline_tests/SYNAPSE_4.lus
index 446522c7..26937607 100644
--- a/offline_tests/SYNAPSE_4.lus
+++ b/offline_tests/SYNAPSE_4.lus
@@ -44,7 +44,7 @@ tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
env : bool;
let
diff --git a/offline_tests/SYNAPSE_4_e8_420_e7_572.lus b/offline_tests/SYNAPSE_4_e8_420_e7_572.lus
index ff4242ea..5bd99024 100644
--- a/offline_tests/SYNAPSE_4_e8_420_e7_572.lus
+++ b/offline_tests/SYNAPSE_4_e8_420_e7_572.lus
@@ -34,7 +34,7 @@ let
tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 4-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
env : bool;
let
diff --git a/offline_tests/SYNAPSE_4_e8_420_e8_1525.lus b/offline_tests/SYNAPSE_4_e8_420_e8_1525.lus
index 0c4ac350..b77bed28 100644
--- a/offline_tests/SYNAPSE_4_e8_420_e8_1525.lus
+++ b/offline_tests/SYNAPSE_4_e8_420_e8_1525.lus
@@ -34,7 +34,7 @@ let
tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
env : bool;
let
diff --git a/offline_tests/SYNAPSE_4_e8_974.lus b/offline_tests/SYNAPSE_4_e8_974.lus
index b4ab9e44..e589b510 100644
--- a/offline_tests/SYNAPSE_4_e8_974.lus
+++ b/offline_tests/SYNAPSE_4_e8_974.lus
@@ -34,7 +34,7 @@ let
tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
env : bool;
let
diff --git a/offline_tests/SYNAPSE_all.lus b/offline_tests/SYNAPSE_all.lus
index 5cedce95..242cd743 100644
--- a/offline_tests/SYNAPSE_all.lus
+++ b/offline_tests/SYNAPSE_all.lus
@@ -48,7 +48,7 @@ tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
env : bool;
let
diff --git a/offline_tests/SYNAPSE_all_e8_251.lus b/offline_tests/SYNAPSE_all_e8_251.lus
index 04e45355..401f4b4e 100644
--- a/offline_tests/SYNAPSE_all_e8_251.lus
+++ b/offline_tests/SYNAPSE_all_e8_251.lus
@@ -37,7 +37,7 @@ let
tel
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
returns( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
env : bool;
let
diff --git a/offline_tests/_6counters_e8_371_e2_80.lus b/offline_tests/_6counters_e8_371_e2_80.lus
index a66d91cc..e2bde05b 100644
--- a/offline_tests/_6counters_e8_371_e2_80.lus
+++ b/offline_tests/_6counters_e8_371_e2_80.lus
@@ -17,7 +17,7 @@ let
tel
node top (x:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var a,b:bool;
let
OK = a=b;
diff --git a/offline_tests/car_1.lus b/offline_tests/car_1.lus
index 4a91ae6b..7724d512 100644
--- a/offline_tests/car_1.lus
+++ b/offline_tests/car_1.lus
@@ -35,7 +35,7 @@ let
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_2.lus b/offline_tests/car_2.lus
index cc9667b2..29cff96d 100644
--- a/offline_tests/car_2.lus
+++ b/offline_tests/car_2.lus
@@ -37,7 +37,7 @@ tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_3.lus b/offline_tests/car_3.lus
index 73d2a280..c2db03c2 100644
--- a/offline_tests/car_3.lus
+++ b/offline_tests/car_3.lus
@@ -37,7 +37,7 @@ tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_3_e2_695.lus b/offline_tests/car_3_e2_695.lus
index 76670ccc..b06a55f5 100644
--- a/offline_tests/car_3_e2_695.lus
+++ b/offline_tests/car_3_e2_695.lus
@@ -27,7 +27,7 @@ let
bump = dist = 10;
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_3_e2_777.lus b/offline_tests/car_3_e2_777.lus
index 76670ccc..b06a55f5 100644
--- a/offline_tests/car_3_e2_777.lus
+++ b/offline_tests/car_3_e2_777.lus
@@ -27,7 +27,7 @@ let
bump = dist = 10;
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_3_e7_626.lus b/offline_tests/car_3_e7_626.lus
index 21500249..c7da573c 100644
--- a/offline_tests/car_3_e7_626.lus
+++ b/offline_tests/car_3_e7_626.lus
@@ -27,7 +27,7 @@ let
bump = dist = 10;
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_3_e8_33.lus b/offline_tests/car_3_e8_33.lus
index 56781633..88720c0e 100644
--- a/offline_tests/car_3_e8_33.lus
+++ b/offline_tests/car_3_e8_33.lus
@@ -27,7 +27,7 @@ let
bump = dist = 10;
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_3_e8_33_e2_1010.lus b/offline_tests/car_3_e8_33_e2_1010.lus
index 1fb08969..a9a4d34c 100644
--- a/offline_tests/car_3_e8_33_e2_1010.lus
+++ b/offline_tests/car_3_e8_33_e2_1010.lus
@@ -27,7 +27,7 @@ let
bump = dist = 10;
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_3_e8_33_e7_220.lus b/offline_tests/car_3_e8_33_e7_220.lus
index 8c28326b..ad0186de 100644
--- a/offline_tests/car_3_e8_33_e7_220.lus
+++ b/offline_tests/car_3_e8_33_e7_220.lus
@@ -27,7 +27,7 @@ let
bump = dist = 10;
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_4.lus b/offline_tests/car_4.lus
index 6a085bfd..6057cd46 100644
--- a/offline_tests/car_4.lus
+++ b/offline_tests/car_4.lus
@@ -35,7 +35,7 @@ let
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_4_e3_57_e4_1047.lus b/offline_tests/car_4_e3_57_e4_1047.lus
index f0f7b4e1..97990ede 100644
--- a/offline_tests/car_4_e3_57_e4_1047.lus
+++ b/offline_tests/car_4_e3_57_e4_1047.lus
@@ -27,7 +27,7 @@ let
bump = dist = 10;
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_4_e3_57_e6_784.lus b/offline_tests/car_4_e3_57_e6_784.lus
index 3a7dadc6..60809ce9 100644
--- a/offline_tests/car_4_e3_57_e6_784.lus
+++ b/offline_tests/car_4_e3_57_e6_784.lus
@@ -27,7 +27,7 @@ let
bump = dist = 10;
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_4_e7_592.lus b/offline_tests/car_4_e7_592.lus
index f9f0bc1e..8322086f 100644
--- a/offline_tests/car_4_e7_592.lus
+++ b/offline_tests/car_4_e7_592.lus
@@ -27,7 +27,7 @@ let
bump = dist = 10;
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_4_e8_118.lus b/offline_tests/car_4_e8_118.lus
index 63450434..9ee81887 100644
--- a/offline_tests/car_4_e8_118.lus
+++ b/offline_tests/car_4_e8_118.lus
@@ -27,7 +27,7 @@ let
bump = dist = 10;
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_all.lus b/offline_tests/car_all.lus
index fdc9a994..b1be79aa 100644
--- a/offline_tests/car_all.lus
+++ b/offline_tests/car_all.lus
@@ -31,7 +31,7 @@ let
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_all_e2_142.lus b/offline_tests/car_all_e2_142.lus
index 793b4511..a4fe26d4 100644
--- a/offline_tests/car_all_e2_142.lus
+++ b/offline_tests/car_all_e2_142.lus
@@ -27,7 +27,7 @@ let
bump = dist = 10;
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_all_e3_1068_e4_275.lus b/offline_tests/car_all_e3_1068_e4_275.lus
index 817b90f3..228d9bb0 100644
--- a/offline_tests/car_all_e3_1068_e4_275.lus
+++ b/offline_tests/car_all_e3_1068_e4_275.lus
@@ -27,7 +27,7 @@ let
bump = dist = 10;
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_all_e8_856.lus b/offline_tests/car_all_e8_856.lus
index 9b9984bd..0d08f572 100644
--- a/offline_tests/car_all_e8_856.lus
+++ b/offline_tests/car_all_e8_856.lus
@@ -27,7 +27,7 @@ let
bump = dist = 10;
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/car_all_e8_856_e2_585.lus b/offline_tests/car_all_e8_856_e2_585.lus
index 748bb844..418f81c0 100644
--- a/offline_tests/car_all_e8_856_e2_585.lus
+++ b/offline_tests/car_all_e8_856_e2_585.lus
@@ -27,7 +27,7 @@ let
bump = dist = 10;
tel
node top(m, s : bool) returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var toofast, stop, bump: bool;
dist, speed, time: int;
move: bool; second, meter: bool;
diff --git a/offline_tests/ccp02.lus b/offline_tests/ccp02.lus
index 4c4780b7..203645ad 100644
--- a/offline_tests/ccp02.lus
+++ b/offline_tests/ccp02.lus
@@ -8,7 +8,7 @@ node top(onOff: bool;
carGear: int ;
carSpeed: real;
validInputs: bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
mode_: int ;
cruiseThrottle: real;
diff --git a/offline_tests/ccp03.lus b/offline_tests/ccp03.lus
index c09270de..74887a35 100644
--- a/offline_tests/ccp03.lus
+++ b/offline_tests/ccp03.lus
@@ -9,7 +9,7 @@ node top(onOff: bool;
carSpeed: real;
validInputs: bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
mode_: int ;
cruiseThrottle: real;
diff --git a/offline_tests/ccp04.lus b/offline_tests/ccp04.lus
index 67af0df1..c010cb42 100644
--- a/offline_tests/ccp04.lus
+++ b/offline_tests/ccp04.lus
@@ -8,7 +8,7 @@ node top(onOff: bool;
carSpeed: real;
validInputs: bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
mode_: int ;
cruiseThrottle: real;
diff --git a/offline_tests/ccp05.lus b/offline_tests/ccp05.lus
index b9e523fe..83a3eccb 100644
--- a/offline_tests/ccp05.lus
+++ b/offline_tests/ccp05.lus
@@ -8,7 +8,7 @@ node top(onOff: bool;
carSpeed: real;
validInputs: bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
mode_: int ;
cruiseThrottle: real;
diff --git a/offline_tests/ccp06.lus b/offline_tests/ccp06.lus
index 64752e0a..a11e2451 100644
--- a/offline_tests/ccp06.lus
+++ b/offline_tests/ccp06.lus
@@ -9,7 +9,7 @@ node top(onOff: bool;
carSpeed: real;
validInputs: bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
mode_: int ;
cruiseThrottle: real;
diff --git a/offline_tests/ccp07.lus b/offline_tests/ccp07.lus
index 6b76d4b7..c22dea3c 100644
--- a/offline_tests/ccp07.lus
+++ b/offline_tests/ccp07.lus
@@ -9,7 +9,7 @@ node top(onOff: bool;
carSpeed: real;
validInputs: bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
mode_: int ;
cruiseThrottle: real;
diff --git a/offline_tests/ccp09.lus b/offline_tests/ccp09.lus
index d34ca65c..93e240eb 100644
--- a/offline_tests/ccp09.lus
+++ b/offline_tests/ccp09.lus
@@ -9,7 +9,7 @@ node top(onOff: bool;
carSpeed: real;
validInputs: bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
mode_: int ;
cruiseThrottle: real;
diff --git a/offline_tests/ccp15.lus b/offline_tests/ccp15.lus
index 1816a1bf..ef1dadd9 100644
--- a/offline_tests/ccp15.lus
+++ b/offline_tests/ccp15.lus
@@ -9,7 +9,7 @@ node top(onOff: bool;
carSpeed: real;
validInputs: bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
mode_: int ;
cruiseThrottle: real;
diff --git a/offline_tests/ccp16.lus b/offline_tests/ccp16.lus
index 49dc938a..f46f87e3 100644
--- a/offline_tests/ccp16.lus
+++ b/offline_tests/ccp16.lus
@@ -9,7 +9,7 @@ node top(onOff: bool;
carSpeed: real;
validInputs: bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
mode_: int ;
cruiseThrottle: real;
diff --git a/offline_tests/ccp19.lus b/offline_tests/ccp19.lus
index 593c5a10..bf480be0 100644
--- a/offline_tests/ccp19.lus
+++ b/offline_tests/ccp19.lus
@@ -9,7 +9,7 @@ node top(onOff: bool;
carSpeed: real;
validInputs: bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
mode_: int ;
cruiseThrottle: real;
diff --git a/offline_tests/cd.lus b/offline_tests/cd.lus
index d8a6aaa3..ec4e03d0 100644
--- a/offline_tests/cd.lus
+++ b/offline_tests/cd.lus
@@ -31,7 +31,7 @@ let
tel
node top(diff:int) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 10-induction;
var speed: int;
plus,minus,realistic: bool;
let
diff --git a/offline_tests/counters.lus b/offline_tests/counters.lus
index 722ef6a9..50fbd314 100644
--- a/offline_tests/counters.lus
+++ b/offline_tests/counters.lus
@@ -45,7 +45,7 @@ tel
node top (x:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 5-induction;
var a,b,d:bool;
s:int;
OK1,OK2,OK3: bool;
diff --git a/offline_tests/cruise_controller_01.lus b/offline_tests/cruise_controller_01.lus
index bb73b0a7..d7487fdf 100644
--- a/offline_tests/cruise_controller_01.lus
+++ b/offline_tests/cruise_controller_01.lus
@@ -10,7 +10,7 @@ node top(onOff: bool;
validInputs: bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
mode_: int;
cruiseThrottle: real;
diff --git a/offline_tests/cruise_controller_02.lus b/offline_tests/cruise_controller_02.lus
index db58987b..f0d02c50 100644
--- a/offline_tests/cruise_controller_02.lus
+++ b/offline_tests/cruise_controller_02.lus
@@ -10,7 +10,7 @@ node top(onOff: bool;
validInputs: bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
mode_: int;
cruiseThrottle: real;
diff --git a/offline_tests/cruise_controller_03.lus b/offline_tests/cruise_controller_03.lus
index c0a9c73d..e4b00e9f 100644
--- a/offline_tests/cruise_controller_03.lus
+++ b/offline_tests/cruise_controller_03.lus
@@ -10,7 +10,7 @@ node top(onOff: bool;
validInputs: bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
mode_: int;
cruiseThrottle: real;
diff --git a/offline_tests/cruise_controller_04.lus b/offline_tests/cruise_controller_04.lus
index b80f933b..0cbe8e63 100644
--- a/offline_tests/cruise_controller_04.lus
+++ b/offline_tests/cruise_controller_04.lus
@@ -10,7 +10,7 @@ node top(onOff: bool;
validInputs: bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
mode_: int;
cruiseThrottle: real;
diff --git a/offline_tests/cruise_controller_05.lus b/offline_tests/cruise_controller_05.lus
index 3720463d..f211180f 100644
--- a/offline_tests/cruise_controller_05.lus
+++ b/offline_tests/cruise_controller_05.lus
@@ -10,7 +10,7 @@ node top(onOff: bool;
validInputs: bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
mode_: int;
cruiseThrottle: real;
diff --git a/offline_tests/cruise_controller_06.lus b/offline_tests/cruise_controller_06.lus
index 433fe208..4af58247 100644
--- a/offline_tests/cruise_controller_06.lus
+++ b/offline_tests/cruise_controller_06.lus
@@ -10,7 +10,7 @@ node top(onOff: bool;
validInputs: bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
mode_: int;
cruiseThrottle: real;
diff --git a/offline_tests/cruise_controller_07.lus b/offline_tests/cruise_controller_07.lus
index 7730678e..521d44e8 100644
--- a/offline_tests/cruise_controller_07.lus
+++ b/offline_tests/cruise_controller_07.lus
@@ -10,7 +10,7 @@ node top(onOff: bool;
validInputs: bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
mode_: int;
cruiseThrottle: real;
diff --git a/offline_tests/cruise_controller_11.lus b/offline_tests/cruise_controller_11.lus
index 92cb8ed7..b9cfbf5d 100644
--- a/offline_tests/cruise_controller_11.lus
+++ b/offline_tests/cruise_controller_11.lus
@@ -10,7 +10,7 @@ node top(onOff: bool;
validInputs: bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
mode_: int;
cruiseThrottle: real;
diff --git a/offline_tests/cruise_controller_13.lus b/offline_tests/cruise_controller_13.lus
index b8c0be1e..a688b0b1 100644
--- a/offline_tests/cruise_controller_13.lus
+++ b/offline_tests/cruise_controller_13.lus
@@ -10,7 +10,7 @@ node top(onOff: bool;
validInputs: bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
mode_: int;
cruiseThrottle: real;
diff --git a/offline_tests/durationThm_1_e2_3.lus b/offline_tests/durationThm_1_e2_3.lus
index 6870dfe4..45bae14c 100644
--- a/offline_tests/durationThm_1_e2_3.lus
+++ b/offline_tests/durationThm_1_e2_3.lus
@@ -8,7 +8,7 @@ let
age_of_p = 0 -> if pre(p) then pre(age_of_p) -1+ 1 else 0;
tel
node top (ik, im: int; p, q, r : bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var k,m : int;
env : bool;
let
diff --git a/offline_tests/durationThm_1_e3_389_e4_294.lus b/offline_tests/durationThm_1_e3_389_e4_294.lus
index 7c9ae780..d0e84ee4 100644
--- a/offline_tests/durationThm_1_e3_389_e4_294.lus
+++ b/offline_tests/durationThm_1_e3_389_e4_294.lus
@@ -8,7 +8,7 @@ let
age_of_p = 0 -> if pre(p) then pre(age_of_p) +1- 1 else 0;
tel
node top (ik, im: int; p, q, r : bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var k,m : int;
env : bool;
let
diff --git a/offline_tests/durationThm_1_e7_217_e2_352.lus b/offline_tests/durationThm_1_e7_217_e2_352.lus
index 29596418..3af57bdb 100644
--- a/offline_tests/durationThm_1_e7_217_e2_352.lus
+++ b/offline_tests/durationThm_1_e7_217_e2_352.lus
@@ -8,7 +8,7 @@ let
age_of_p = 0 -> if pre(p) then pre(age_of_p) -1+ 1 else 0;
tel
node top (ik, im: int; p, q, r : bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 7-induction;
var k,m : int;
env : bool;
let
diff --git a/offline_tests/durationThm_2_e2_63.lus b/offline_tests/durationThm_2_e2_63.lus
index 11fcf68c..44d06ff2 100644
--- a/offline_tests/durationThm_2_e2_63.lus
+++ b/offline_tests/durationThm_2_e2_63.lus
@@ -8,7 +8,7 @@ let
age_of_p = 0 -> if pre(p) then pre(age_of_p) -1+ 1 else 0;
tel
node top (k0: int; p, q, r, t : bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var k: int;
env : bool;
let
diff --git a/offline_tests/durationThm_2_e3_329_e4_1.lus b/offline_tests/durationThm_2_e3_329_e4_1.lus
index 5bd482a0..bf9a367f 100644
--- a/offline_tests/durationThm_2_e3_329_e4_1.lus
+++ b/offline_tests/durationThm_2_e3_329_e4_1.lus
@@ -8,7 +8,7 @@ let
age_of_p = 0 -> if pre(p) then pre(age_of_p) +1- 1 else 0;
tel
node top (k0: int; p, q, r, t : bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var k: int;
env : bool;
let
diff --git a/offline_tests/durationThm_2_e7_145_e2_169.lus b/offline_tests/durationThm_2_e7_145_e2_169.lus
index d9e7cded..a5c0dd84 100644
--- a/offline_tests/durationThm_2_e7_145_e2_169.lus
+++ b/offline_tests/durationThm_2_e7_145_e2_169.lus
@@ -8,7 +8,7 @@ let
age_of_p = 0 -> if pre(p) then pre(age_of_p) -1+ 1 else 0;
tel
node top (k0: int; p, q, r, t : bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 8-induction;
var k: int;
env : bool;
let
diff --git a/offline_tests/durationThm_3_e2_148.lus b/offline_tests/durationThm_3_e2_148.lus
index 5243cc18..6a28c7c6 100644
--- a/offline_tests/durationThm_3_e2_148.lus
+++ b/offline_tests/durationThm_3_e2_148.lus
@@ -8,7 +8,7 @@ let
age_of_p = 0 -> if pre(p) then pre(age_of_p) -1+ 1 else 0;
tel
node top (k0, m0: int; p, q : bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var k,m: int;
env : bool;
let
diff --git a/offline_tests/durationThm_3_e2_63.lus b/offline_tests/durationThm_3_e2_63.lus
index 5243cc18..6a28c7c6 100644
--- a/offline_tests/durationThm_3_e2_63.lus
+++ b/offline_tests/durationThm_3_e2_63.lus
@@ -8,7 +8,7 @@ let
age_of_p = 0 -> if pre(p) then pre(age_of_p) -1+ 1 else 0;
tel
node top (k0, m0: int; p, q : bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var k,m: int;
env : bool;
let
diff --git a/offline_tests/durationThm_3_e3_207.lus b/offline_tests/durationThm_3_e3_207.lus
index 37773db0..0e4f6c2d 100644
--- a/offline_tests/durationThm_3_e3_207.lus
+++ b/offline_tests/durationThm_3_e3_207.lus
@@ -8,7 +8,7 @@ let
age_of_p = 0 -> if pre(p) then pre(age_of_p) - 1 else 0;
tel
node top (k0, m0: int; p, q : bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var k,m: int;
env : bool;
let
diff --git a/offline_tests/durationThm_3_e3_442.lus b/offline_tests/durationThm_3_e3_442.lus
index 37773db0..0e4f6c2d 100644
--- a/offline_tests/durationThm_3_e3_442.lus
+++ b/offline_tests/durationThm_3_e3_442.lus
@@ -8,7 +8,7 @@ let
age_of_p = 0 -> if pre(p) then pre(age_of_p) - 1 else 0;
tel
node top (k0, m0: int; p, q : bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var k,m: int;
env : bool;
let
diff --git a/offline_tests/durationThm_3_e3_442_e4_165.lus b/offline_tests/durationThm_3_e3_442_e4_165.lus
index 39f63ca0..a416e58f 100644
--- a/offline_tests/durationThm_3_e3_442_e4_165.lus
+++ b/offline_tests/durationThm_3_e3_442_e4_165.lus
@@ -8,7 +8,7 @@ let
age_of_p = 0 -> if pre(p) then pre(age_of_p) +1- 1 else 0;
tel
node top (k0, m0: int; p, q : bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var k,m: int;
env : bool;
let
diff --git a/offline_tests/durationThm_3_e3_442_e5_260.lus b/offline_tests/durationThm_3_e3_442_e5_260.lus
index 649de53e..6ef577a6 100644
--- a/offline_tests/durationThm_3_e3_442_e5_260.lus
+++ b/offline_tests/durationThm_3_e3_442_e5_260.lus
@@ -8,7 +8,7 @@ let
age_of_p = 0 -> if pre(p) then pre(age_of_p) -1- 1 else 0;
tel
node top (k0, m0: int; p, q : bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var k,m: int;
env : bool;
let
diff --git a/offline_tests/durationThm_3_e7_334_e2_62.lus b/offline_tests/durationThm_3_e7_334_e2_62.lus
index fb3000b6..5bf36dd2 100644
--- a/offline_tests/durationThm_3_e7_334_e2_62.lus
+++ b/offline_tests/durationThm_3_e7_334_e2_62.lus
@@ -8,7 +8,7 @@ let
age_of_p = 0 -> if pre(p) then pre(age_of_p) -1+ 1 else 0;
tel
node top (k0, m0: int; p, q : bool) returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 4-induction;
var k,m: int;
env : bool;
let
diff --git a/offline_tests/ex3_e7_590_e7_590.lus b/offline_tests/ex3_e7_590_e7_590.lus
index ac5941b3..0c8868d4 100644
--- a/offline_tests/ex3_e7_590_e7_590.lus
+++ b/offline_tests/ex3_e7_590_e7_590.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var late,early: bool;
let
(late,early) = speed(beacon,second);
diff --git a/offline_tests/ex3_e7_655.lus b/offline_tests/ex3_e7_655.lus
index 9320f6c7..e7e1dffb 100644
--- a/offline_tests/ex3_e7_655.lus
+++ b/offline_tests/ex3_e7_655.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var late,early: bool;
let
(late,early) = speed(beacon,second);
diff --git a/offline_tests/ex3_e8_381.lus b/offline_tests/ex3_e8_381.lus
index 397a66a1..693fc6ae 100644
--- a/offline_tests/ex3_e8_381.lus
+++ b/offline_tests/ex3_e8_381.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var late,early: bool;
let
(late,early) = speed(beacon,second);
diff --git a/offline_tests/ex3_e8_381_e7_224.lus b/offline_tests/ex3_e8_381_e7_224.lus
index 709872be..ed76cdb1 100644
--- a/offline_tests/ex3_e8_381_e7_224.lus
+++ b/offline_tests/ex3_e8_381_e7_224.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var late,early: bool;
let
(late,early) = speed(beacon,second);
diff --git a/offline_tests/ex3_e8_381_e8_477.lus b/offline_tests/ex3_e8_381_e8_477.lus
index 90ec6cb4..db939b2f 100644
--- a/offline_tests/ex3_e8_381_e8_477.lus
+++ b/offline_tests/ex3_e8_381_e8_477.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var late,early: bool;
let
(late,early) = speed(beacon,second);
diff --git a/offline_tests/fast_1.lus b/offline_tests/fast_1.lus
index 0cc5333a..adf76040 100644
--- a/offline_tests/fast_1.lus
+++ b/offline_tests/fast_1.lus
@@ -127,7 +127,7 @@ tel
node top (igsw, ccd, cconoff, bpa, cccanc, battok, gearok,
qfok, sdok, accok, ccseti, ccsetd, ccr: bool; vs: int)
returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
ccont, cca: bool;
env : bool;
diff --git a/offline_tests/fast_1_e8_747_e8_1041.lus b/offline_tests/fast_1_e8_747_e8_1041.lus
index 6a52b5ac..c3078830 100644
--- a/offline_tests/fast_1_e8_747_e8_1041.lus
+++ b/offline_tests/fast_1_e8_747_e8_1041.lus
@@ -72,7 +72,7 @@ tel
node top (igsw, ccd, cconoff, bpa, cccanc, battok, gearok,
qfok, sdok, accok, ccseti, ccsetd, ccr: bool; vs: int)
returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
ccont, cca: bool;
env : bool;
diff --git a/offline_tests/fast_1_e8_751.lus b/offline_tests/fast_1_e8_751.lus
index 7f6342e7..36ed799d 100644
--- a/offline_tests/fast_1_e8_751.lus
+++ b/offline_tests/fast_1_e8_751.lus
@@ -72,7 +72,7 @@ tel
node top (igsw, ccd, cconoff, bpa, cccanc, battok, gearok,
qfok, sdok, accok, ccseti, ccsetd, ccr: bool; vs: int)
returns (OK : bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
ccont, cca: bool;
env : bool;
diff --git a/offline_tests/fast_2.lus b/offline_tests/fast_2.lus
index 2c1dd082..e13821c1 100644
--- a/offline_tests/fast_2.lus
+++ b/offline_tests/fast_2.lus
@@ -128,7 +128,7 @@ tel
node top (igsw, ccd, cconoff, bpa, cccanc, battok, gearok,
qfok, sdok, accok, ccseti, ccsetd, ccr: bool; vs: int)
returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
p1, p2, p3, p4: bool;
ccont, cca: bool;
diff --git a/offline_tests/fast_2_e8_460_e8_1920.lus b/offline_tests/fast_2_e8_460_e8_1920.lus
index 112226e4..3cee21b4 100644
--- a/offline_tests/fast_2_e8_460_e8_1920.lus
+++ b/offline_tests/fast_2_e8_460_e8_1920.lus
@@ -72,7 +72,7 @@ tel
node top (igsw, ccd, cconoff, bpa, cccanc, battok, gearok,
qfok, sdok, accok, ccseti, ccsetd, ccr: bool; vs: int)
returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
p1, p2, p3, p4: bool;
ccont, cca: bool;
diff --git a/offline_tests/fast_2_e8_976.lus b/offline_tests/fast_2_e8_976.lus
index a75e8768..4a82683a 100644
--- a/offline_tests/fast_2_e8_976.lus
+++ b/offline_tests/fast_2_e8_976.lus
@@ -72,7 +72,7 @@ tel
node top (igsw, ccd, cconoff, bpa, cccanc, battok, gearok,
qfok, sdok, accok, ccseti, ccsetd, ccr: bool; vs: int)
returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
p1, p2, p3, p4: bool;
ccont, cca: bool;
diff --git a/offline_tests/heater4.lus b/offline_tests/heater4.lus
index 4f09bceb..5e75eacc 100644
--- a/offline_tests/heater4.lus
+++ b/offline_tests/heater4.lus
@@ -1,5 +1,5 @@
node top(millisecond : bool) returns (open_light : bool)
-(*@ contract guarantee open_light; *)
+(*@ contract guarantee open_light by 2-induction; *)
let
automaton command_control
state Open :
@@ -11,5 +11,5 @@ let
let
open_light = false;
tel
-
+ --%PROPERTY open_light;
tel
diff --git a/offline_tests/hysteresis_1.lus b/offline_tests/hysteresis_1.lus
index a83d56cb..c741b3ea 100644
--- a/offline_tests/hysteresis_1.lus
+++ b/offline_tests/hysteresis_1.lus
@@ -27,7 +27,7 @@ let
tel
node top( beacon, second : bool ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var late, early : bool;
let
( late, early ) = speed( beacon, second );
diff --git a/offline_tests/hysteresis_2.lus b/offline_tests/hysteresis_2.lus
index fce911b6..c3c93cde 100644
--- a/offline_tests/hysteresis_2.lus
+++ b/offline_tests/hysteresis_2.lus
@@ -27,7 +27,7 @@ let
tel
node top( beacon, second : bool ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var late, early : bool;
let
( late, early ) = speed( beacon, second );
diff --git a/offline_tests/hysteresis_3.lus b/offline_tests/hysteresis_3.lus
index 3b6e8acc..8c98a641 100644
--- a/offline_tests/hysteresis_3.lus
+++ b/offline_tests/hysteresis_3.lus
@@ -27,7 +27,7 @@ let
tel
node top( beacon, second : bool ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var late, early : bool;
let
( late, early ) = speed( beacon, second );
diff --git a/offline_tests/hysteresis_all.lus b/offline_tests/hysteresis_all.lus
index 70df17dc..83b0f86e 100644
--- a/offline_tests/hysteresis_all.lus
+++ b/offline_tests/hysteresis_all.lus
@@ -27,7 +27,7 @@ let
tel
node top( beacon, second : bool ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var late, early : bool;
let
( late, early ) = speed( beacon, second );
diff --git a/offline_tests/ignored b/offline_tests/ignored
index df606713..9718c5a5 100644
--- a/offline_tests/ignored
+++ b/offline_tests/ignored
@@ -1,285 +1,697 @@
-DRAGON_10_e1_3587_e3_2749.lus
-DRAGON_10_e1_3587_e7_872.lus
-DRAGON_10_e1_998.lus
-DRAGON_10_e2_2785_e3_1744.lus
-DRAGON_10_e2_402.lus
-DRAGON_10_e3_144_e5_2046.lus
-DRAGON_10_e3_144_e7_523.lus
-DRAGON_10_e3_3429.lus
-DRAGON_10_e7_3861_e2_1020.lus
-DRAGON_10_e7_3861_e7_2180.lus
-DRAGON_10.lus
-DRAGON_11_e1_2450_e1_5887.lus
-DRAGON_11_e1_2450_e2_1483.lus
-DRAGON_11_e1_2450_e3_2330.lus
-DRAGON_11_e1_2450_e7_5791.lus
-DRAGON_11_e1_2450.lus
-DRAGON_11_e2_1678_e1_3565.lus
-DRAGON_11_e2_5396_e3_282.lus
-DRAGON_11_e3_382_e1_505.lus
-DRAGON_11_e3_382_e4_4421.lus
-DRAGON_11.lus
-DRAGON_12_e1_4640_e7_128.lus
-DRAGON_12_e2_1618_e1_6030.lus
-DRAGON_12_e2_1618_e2_138.lus
-DRAGON_12_e2_1618_e3_2012.lus
-DRAGON_12_e2_1618_e7_4732.lus
-DRAGON_12_e2_1618.lus
-DRAGON_12.lus
-DRAGON_13_e3_1418_e3_2761.lus
-DRAGON_13_e7_2336_e1_541.lus
-DRAGON_13_e7_2336_e2_1255.lus
-DRAGON_13_e7_2336_e3_3117.lus
-DRAGON_13_e7_2336_e7_685.lus
-DRAGON_13_e7_2336.lus
-DRAGON_13.lus
-DRAGON_14_e1_5710.lus
-DRAGON_14_e2_3606.lus
-DRAGON_14_e3_1259_e1_5798.lus
-DRAGON_14_e3_5120.lus
-DRAGON_14_e7_3162_e1_3998.lus
-DRAGON_14_e7_3162_e2_753.lus
-DRAGON_14_e7_3162_e3_4298.lus
-DRAGON_14_e7_3162_e7_3528.lus
-DRAGON_14_e7_3162.lus
-DRAGON_14.lus
-DRAGON_1_e1_14612_e1_268_e7_501.lus
-DRAGON_1_e1_14612_e2_2653_e7_4370.lus
-DRAGON_1_e1_3184_e7_1888.lus
-DRAGON_1_e1_5070.lus
-DRAGON_1_e2_1997_e7_3613_e2_3409.lus
-DRAGON_1_e2_1997.lus
-DRAGON_1_e3_11891_e7_4569_e4_4881.lus
-DRAGON_1.lus
-DRAGON_2_e1_2316.lus
-DRAGON_2_e2_3183_e1_2644.lus
-DRAGON_2_e2_3183_e2_3580.lus
-DRAGON_2_e2_3183_e3_5972.lus
-DRAGON_2_e2_4481.lus
-DRAGON_2_e7_25_e1_154.lus
-DRAGON_2_e7_25_e2_5340.lus
-DRAGON_2_e7_25_e3_829.lus
-DRAGON_2_e7_25_e7_4469.lus
-DRAGON_2_e7_25_e8_3171.lus
-DRAGON_2_e7_25.lus
-DRAGON_2.lus
-DRAGON_3_e1_4783_e1_3755.lus
-DRAGON_3_e1_4783_e2_158.lus
-DRAGON_3_e1_4783_e3_511.lus
-DRAGON_3_e1_4783_e7_4070.lus
-DRAGON_3_e1_4783.lus
-DRAGON_3_e2_5343_e1_988.lus
-DRAGON_3_e3_3846.lus
-DRAGON_3_e3_5422_e1_2288.lus
-DRAGON_3_e3_5422_e2_3135.lus
-DRAGON_3_e7_4884.lus
-DRAGON_3.lus
-DRAGON_4_e1_4312.lus
-DRAGON_4_e2_2799_e1_1303.lus
-DRAGON_4_e2_2799_e2_2251.lus
-DRAGON_4_e2_2799_e3_1915.lus
-DRAGON_4_e2_2799_e7_2499.lus
-DRAGON_4_e2_2799.lus
-DRAGON_4_e3_1540_e1_5048.lus
-DRAGON_4_e3_4133.lus
-DRAGON_4_e7_2329_e3_4574.lus
-DRAGON_4_e7_2329_e7_3856.lus
-DRAGON_4_e7_2329.lus
-DRAGON_4.lus
-DRAGON_5_e1_1835.lus
-DRAGON_5_e2_3018_e2_936.lus
-DRAGON_5_e7_2017_e1_5832.lus
-DRAGON_5_e7_2017_e2_664.lus
-DRAGON_5_e7_2017_e3_1763.lus
-DRAGON_5_e7_2017_e7_2326.lus
-DRAGON_5_e7_2017.lus
-DRAGON_5.lus
-DRAGON_6_e7_5046_e7_3623.lus
-DRAGON_6.lus
-DRAGON_7_e2_2872_e2_5844.lus
-DRAGON_7_e2_2872_e3_2640.lus
-DRAGON_7_e7_3157_e2_2082.lus
-DRAGON_7.lus
-DRAGON_8_e2_3896_e3_3125.lus
-DRAGON_8_e3_786_e7_4541.lus
-DRAGON_8_e3_786.lus
-DRAGON_8_e7_3752.lus
-DRAGON_8.lus
-DRAGON_9_e7_1843_e1_5434.lus
-DRAGON_9_e7_1843_e2_1145.lus
-DRAGON_9_e7_1843_e3_5316.lus
-DRAGON_9_e7_1843_e7_2225.lus
-DRAGON_9_e7_1843.lus
-DRAGON_9.lus
-DRAGON_all2_e2_2073_e8_3691.lus
-DRAGON_all2_e3_4612_e1_6463.lus
-DRAGON_all2_e3_4612_e2_5774.lus
-DRAGON_all2_e3_4612_e3_1543.lus
-DRAGON_all2_e3_4612_e4_3719.lus
-DRAGON_all2_e3_4612_e5_3642.lus
-DRAGON_all2_e3_4612_e8_5861.lus
-DRAGON_all2_e7_5406_e1_6690.lus
-DRAGON_all2_e7_5406_e2_3084.lus
-DRAGON_all2_e7_5406_e3_506.lus
-DRAGON_all2_e7_5406_e7_6697.lus
-DRAGON_all2_e7_5406.lus
-DRAGON_all2_e8_4626.lus
-DRAGON_all2_e8_5504_e1_4719.lus
-DRAGON_all2_e8_5504_e2_1598.lus
-DRAGON_all2_e8_5504_e7_579.lus
-DRAGON_all2_e8_5504.lus
-DRAGON_all2.lus
-DRAGON_all_e1_4022_e1_1759.lus
-DRAGON_all_e1_4022_e2_267.lus
-DRAGON_all_e1_4022_e3_3628.lus
-DRAGON_all_e1_4022_e7_2886.lus
-DRAGON_all_e1_4037.lus
-DRAGON_all_e2_6104_e1_6205.lus
-DRAGON_all_e2_6104_e2_3308.lus
-DRAGON_all_e2_6104_e3_2607.lus
-DRAGON_all_e2_6104.lus
-DRAGON_all_e3_4821_e1_1318.lus
-DRAGON_all_e3_4821_e2_1089.lus
-DRAGON_all_e3_4821_e4_1791.lus
-DRAGON_all_e3_4821_e5_1536.lus
-DRAGON_all_e3_5957.lus
-DRAGON_all_e7_1941_e2_6086.lus
-DRAGON_all_e7_4065.lus
-DRAGON_all.lus
-Delay2_PP.LUSTREC.lus
-Delay5_PP.LUSTREC.lus
-DelayBus_PP.LUSTREC.lus
-FIREFLY_10_e7_919_e2_3192.lus
-FIREFLY_10.lus
-FIREFLY_11_e1_3457.lus
-FIREFLY_11_e3_2076_e1_1270.lus
-FIREFLY_11.lus
-FIREFLY_1_e1_1092_e1_1486.lus
-FIREFLY_1_e1_1092_e2_1853.lus
-FIREFLY_1_e1_1092_e3_389.lus
-FIREFLY_1_e1_1092_e7_1119.lus
-FIREFLY_1_e1_1092.lus
-FIREFLY_1.lus
-FIREFLY_2_e3_151_e3_1540.lus
-FIREFLY_2.lus
-FIREFLY_3_e2_2236_e1_2305.lus
-FIREFLY_3_e2_2236_e2_1058.lus
-FIREFLY_3_e2_2236_e3_2657.lus
-FIREFLY_3_e2_2236_e7_3681.lus
-FIREFLY_3_e2_2236.lus
-FIREFLY_3.lus
-FIREFLY_4_e3_3511_e1_2375.lus
-FIREFLY_4_e3_3511_e2_1923.lus
-FIREFLY_4_e3_3511_e3_422.lus
-FIREFLY_4_e3_3511_e4_1464.lus
-FIREFLY_4_e3_3511_e5_3248.lus
-FIREFLY_4_e3_3511_e7_3568.lus
-FIREFLY_4_e3_3511.lus
-FIREFLY_4.lus
-FIREFLY_5_e1_2552_e7_1169.lus
-FIREFLY_5_e2_2229.lus
-FIREFLY_5_e2_2884_e1_2678.lus
-FIREFLY_5_e2_2884_e2_1492.lus
-FIREFLY_5_e2_2884_e3_1882.lus
-FIREFLY_5_e2_2884_e7_3594.lus
-FIREFLY_5_e2_2884.lus
-FIREFLY_5.lus
-FIREFLY_6_e2_3302.lus
-FIREFLY_6.lus
-FIREFLY_7.lus
-FIREFLY_8_e2_1711_e1_1489.lus
-FIREFLY_8_e2_1711_e2_2673.lus
-FIREFLY_8_e2_1711_e3_1753.lus
-FIREFLY_8_e2_1711_e7_1962.lus
-FIREFLY_8_e2_1711.lus
-FIREFLY_8.lus
-FIREFLY_9_e7_170_e3_3647.lus
-FIREFLY_9.lus
-FIREFLY_a3_e1_3233_e1_3123.lus
-FIREFLY_a3_e1_3233_e2_2392.lus
-FIREFLY_a3_e1_3233_e3_2970.lus
-FIREFLY_a3_e1_3233_e7_906.lus
-FIREFLY_a3_e1_3233.lus
-FIREFLY_a3_e2_2086_e1_3235.lus
-FIREFLY_a3_e2_2086_e2_2689.lus
-FIREFLY_a3_e2_2086_e3_2542.lus
-FIREFLY_a3_e2_2086_e7_2614.lus
-FIREFLY_a3_e2_2952.lus
-FIREFLY_a3_e3_314_e1_1979.lus
-FIREFLY_a3_e3_314_e2_2812.lus
-FIREFLY_a3_e3_314_e4_897.lus
-FIREFLY_a3.lus
-FIREFLY_all_e1_1207_e1_1201.lus
-FIREFLY_all_e1_1207_e2_3220.lus
-FIREFLY_all_e1_1207_e3_1928.lus
-FIREFLY_all_e1_1207_e7_156.lus
-FIREFLY_all_e1_3406.lus
-FIREFLY_all_e2_2924_e1_768.lus
-FIREFLY_all_e2_2924_e2_1767.lus
-FIREFLY_all_e2_2924_e3_3946.lus
-FIREFLY_all_e2_2924_e7_3371.lus
-FIREFLY_all_e2_3678.lus
-FIREFLY_all_e3_1600_e1_667.lus
-FIREFLY_all_e3_1600_e2_676.lus
-FIREFLY_all_e3_1600_e3_2055.lus
-FIREFLY_all_e3_1600_e4_2415.lus
-FIREFLY_all_e3_1600_e5_84.lus
-FIREFLY_all_e3_1600_e7_1607.lus
-FIREFLY_all_e3_3496.lus
-FIREFLY_all_e7_1909.lus
-FIREFLY_all.lus
-FIREFLY_luke_1a_e2_284_e1_2924.lus
-FIREFLY_luke_1a_e2_284_e2_2755.lus
-FIREFLY_luke_1a_e2_284_e3_3091.lus
-FIREFLY_luke_1a_e2_284_e7_998.lus
-FIREFLY_luke_1a_e7_3042_e3_1213.lus
-FIREFLY_luke_1a.lus
-FIREFLY_luke_1b_e1_1139_e1_1565.lus
-FIREFLY_luke_1b_e1_1139_e2_2893.lus
-FIREFLY_luke_1b_e1_1139_e3_1839.lus
-FIREFLY_luke_1b_e1_1691.lus
-FIREFLY_luke_1b_e2_3049_e1_946.lus
-FIREFLY_luke_1b_e2_3049_e2_698.lus
-FIREFLY_luke_1b_e2_3049_e3_2697.lus
-FIREFLY_luke_1b_e2_3049.lus
-FIREFLY_luke_1b_e3_671_e1_725.lus
-FIREFLY_luke_1b_e3_671_e2_2131.lus
-FIREFLY_luke_1b_e3_671_e3_941.lus
-FIREFLY_luke_1b_e3_671_e4_147.lus
-FIREFLY_luke_1b_e3_671_e5_1637.lus
-FIREFLY_luke_1b_e3_671_e6_1974.lus
-FIREFLY_luke_1b_e3_671_e7_1882.lus
-FIREFLY_luke_1b_e3_671.lus
-FIREFLY_luke_1b_e7_2574.lus
-FIREFLY_luke_1b_e7_3191_e1_1303.lus
-FIREFLY_luke_1b_e7_3191_e2_1864.lus
-FIREFLY_luke_1b_e7_3191_e3_1250.lus
-FIREFLY_luke_1b_e7_3191_e7_2146.lus
-FIREFLY_luke_1b_e7_3191_e8_2830.lus
-FIREFLY_luke_1b_e7_3191.lus
-FIREFLY_luke_1b.lus
-FIREFLY_luke_2_e2_1375_e1_418.lus
-FIREFLY_luke_2_e7_1826_e8_126.lus
-FIREFLY_luke_2.lus
-FIREFLY_luke_3_e1_2217_e3_1200.lus
-FIREFLY_luke_3.lus
-FIREFLY_luke_4_e2_325.lus
-FIREFLY_luke_4.lus
-FIREFLY_luke_5.lus
-FIREFLY_luke_rt_e1_913_e1_1993.lus
-FIREFLY_luke_rt_e1_913_e2_3353.lus
-FIREFLY_luke_rt_e1_913_e3_2128.lus
-FIREFLY_luke_rt_e1_913_e7_1403.lus
-FIREFLY_luke_rt_e1_913.lus
-FIREFLY_luke_rt_e2_3460_e1_1455.lus
-FIREFLY_luke_rt_e2_3460_e2_2670.lus
-FIREFLY_luke_rt_e2_3460_e3_1333.lus
-FIREFLY_luke_rt_e2_3460_e7_471.lus
-FIREFLY_luke_rt_e2_3460.lus
-FIREFLY_luke_rt_e3_1549.lus
-FIREFLY_luke_rt.lus
-FIREFLY_rt_e3_1770_e2_637.lus
-FIREFLY_rt.lus
-FIREFLY_u1_e2_3403_e2_957.lus
-FIREFLY_u1_e7_3318.lus
-FIREFLY_u1.lus
+DRAGON_1
+DRAGON_10
+DRAGON_10_e1_3587_e3_2749
+DRAGON_10_e1_3587_e7_872
+DRAGON_10_e1_998
+DRAGON_10_e2_2785_e3_1744
+DRAGON_10_e2_402
+DRAGON_10_e3_144_e5_2046
+DRAGON_10_e3_144_e7_523
+DRAGON_10_e3_3429
+DRAGON_10_e7_3861_e2_1020
+DRAGON_10_e7_3861_e7_2180
+DRAGON_11
+DRAGON_11_e1_2450
+DRAGON_11_e1_2450_e1_5887
+DRAGON_11_e1_2450_e2_1483
+DRAGON_11_e1_2450_e3_2330
+DRAGON_11_e1_2450_e7_5791
+DRAGON_11_e2_1678_e1_3565
+DRAGON_11_e2_5396_e3_282
+DRAGON_11_e3_382_e1_505
+DRAGON_11_e3_382_e4_4421
+DRAGON_12
+DRAGON_12_e1_4640_e7_128
+DRAGON_12_e2_1618
+DRAGON_12_e2_1618_e1_6030
+DRAGON_12_e2_1618_e2_138
+DRAGON_12_e2_1618_e3_2012
+DRAGON_12_e2_1618_e7_4732
+DRAGON_13
+DRAGON_13_e3_1418_e3_2761
+DRAGON_13_e7_2336
+DRAGON_13_e7_2336_e1_541
+DRAGON_13_e7_2336_e2_1255
+DRAGON_13_e7_2336_e3_3117
+DRAGON_13_e7_2336_e7_685
+DRAGON_14
+DRAGON_14_e1_5710
+DRAGON_14_e2_3606
+DRAGON_14_e3_1259_e1_5798
+DRAGON_14_e3_5120
+DRAGON_14_e7_3162
+DRAGON_14_e7_3162_e1_3998
+DRAGON_14_e7_3162_e2_753
+DRAGON_14_e7_3162_e3_4298
+DRAGON_14_e7_3162_e7_3528
+DRAGON_1_e1_14612_e1_268_e7_501
+DRAGON_1_e1_14612_e2_2653_e7_4370
+DRAGON_1_e1_3184_e7_1888
+DRAGON_1_e1_5070
+DRAGON_1_e2_1997
+DRAGON_1_e2_1997_e7_3613_e2_3409
+DRAGON_1_e3_11891_e7_4569_e4_4881
+DRAGON_2
+DRAGON_2_e1_2316
+DRAGON_2_e2_3183_e1_2644
+DRAGON_2_e2_3183_e2_3580
+DRAGON_2_e2_3183_e3_5972
+DRAGON_2_e2_4481
+DRAGON_2_e7_25
+DRAGON_2_e7_25_e1_154
+DRAGON_2_e7_25_e2_5340
+DRAGON_2_e7_25_e3_829
+DRAGON_2_e7_25_e7_4469
+DRAGON_2_e7_25_e8_3171
+DRAGON_3
+DRAGON_3_e1_4783
+DRAGON_3_e1_4783_e1_3755
+DRAGON_3_e1_4783_e2_158
+DRAGON_3_e1_4783_e3_511
+DRAGON_3_e1_4783_e7_4070
+DRAGON_3_e2_5343_e1_988
+DRAGON_3_e3_3846
+DRAGON_3_e3_5422_e1_2288
+DRAGON_3_e3_5422_e2_3135
+DRAGON_3_e7_4884
+DRAGON_4
+DRAGON_4_e1_4312
+DRAGON_4_e2_2799
+DRAGON_4_e2_2799_e1_1303
+DRAGON_4_e2_2799_e2_2251
+DRAGON_4_e2_2799_e3_1915
+DRAGON_4_e2_2799_e7_2499
+DRAGON_4_e3_1540_e1_5048
+DRAGON_4_e3_4133
+DRAGON_4_e7_2329
+DRAGON_4_e7_2329_e3_4574
+DRAGON_4_e7_2329_e7_3856
+DRAGON_5
+DRAGON_5_e1_1835
+DRAGON_5_e2_3018_e2_936
+DRAGON_5_e7_2017
+DRAGON_5_e7_2017_e1_5832
+DRAGON_5_e7_2017_e2_664
+DRAGON_5_e7_2017_e3_1763
+DRAGON_5_e7_2017_e7_2326
+DRAGON_6
+DRAGON_6_e7_5046_e7_3623
+DRAGON_7
+DRAGON_7_e2_2872_e2_5844
+DRAGON_7_e2_2872_e3_2640
+DRAGON_7_e7_3157_e2_2082
+DRAGON_8
+DRAGON_8_e2_3896_e3_3125
+DRAGON_8_e3_786
+DRAGON_8_e3_786_e7_4541
+DRAGON_8_e7_3752
+DRAGON_9
+DRAGON_9_e7_1843
+DRAGON_9_e7_1843_e1_5434
+DRAGON_9_e7_1843_e2_1145
+DRAGON_9_e7_1843_e3_5316
+DRAGON_9_e7_1843_e7_2225
+DRAGON_all
+DRAGON_all2
+DRAGON_all2_e2_2073_e8_3691
+DRAGON_all2_e3_4612_e1_6463
+DRAGON_all2_e3_4612_e2_5774
+DRAGON_all2_e3_4612_e3_1543
+DRAGON_all2_e3_4612_e4_3719
+DRAGON_all2_e3_4612_e5_3642
+DRAGON_all2_e3_4612_e8_5861
+DRAGON_all2_e7_5406
+DRAGON_all2_e7_5406_e1_6690
+DRAGON_all2_e7_5406_e2_3084
+DRAGON_all2_e7_5406_e3_506
+DRAGON_all2_e7_5406_e7_6697
+DRAGON_all2_e8_4626
+DRAGON_all2_e8_5504
+DRAGON_all2_e8_5504_e1_4719
+DRAGON_all2_e8_5504_e2_1598
+DRAGON_all2_e8_5504_e7_579
+DRAGON_all_e1_4022_e1_1759
+DRAGON_all_e1_4022_e2_267
+DRAGON_all_e1_4022_e3_3628
+DRAGON_all_e1_4022_e7_2886
+DRAGON_all_e1_4037
+DRAGON_all_e2_6104
+DRAGON_all_e2_6104_e1_6205
+DRAGON_all_e2_6104_e2_3308
+DRAGON_all_e2_6104_e3_2607
+DRAGON_all_e3_4821_e1_1318
+DRAGON_all_e3_4821_e2_1089
+DRAGON_all_e3_4821_e4_1791
+DRAGON_all_e3_4821_e5_1536
+DRAGON_all_e3_5957
+DRAGON_all_e7_1941_e2_6086
+DRAGON_all_e7_4065
+FIREFLY_1
+FIREFLY_10
+FIREFLY_10_e7_919_e2_3192
+FIREFLY_11
+FIREFLY_11_e1_3457
+FIREFLY_11_e3_2076_e1_1270
+FIREFLY_1_e1_1092
+FIREFLY_1_e1_1092_e1_1486
+FIREFLY_1_e1_1092_e2_1853
+FIREFLY_1_e1_1092_e3_389
+FIREFLY_1_e1_1092_e7_1119
+FIREFLY_2
+FIREFLY_2_e3_151_e3_1540
+FIREFLY_3
+FIREFLY_3_e2_2236
+FIREFLY_3_e2_2236_e1_2305
+FIREFLY_3_e2_2236_e2_1058
+FIREFLY_3_e2_2236_e3_2657
+FIREFLY_3_e2_2236_e7_3681
+FIREFLY_4
+FIREFLY_4_e3_3511
+FIREFLY_4_e3_3511_e1_2375
+FIREFLY_4_e3_3511_e2_1923
+FIREFLY_4_e3_3511_e3_422
+FIREFLY_4_e3_3511_e4_1464
+FIREFLY_4_e3_3511_e5_3248
+FIREFLY_4_e3_3511_e7_3568
+FIREFLY_5
+FIREFLY_5_e1_2552_e7_1169
+FIREFLY_5_e2_2229
+FIREFLY_5_e2_2884
+FIREFLY_5_e2_2884_e1_2678
+FIREFLY_5_e2_2884_e2_1492
+FIREFLY_5_e2_2884_e3_1882
+FIREFLY_5_e2_2884_e7_3594
+FIREFLY_6
+FIREFLY_6_e2_3302
+FIREFLY_7
+FIREFLY_8
+FIREFLY_8_e2_1711
+FIREFLY_8_e2_1711_e1_1489
+FIREFLY_8_e2_1711_e2_2673
+FIREFLY_8_e2_1711_e3_1753
+FIREFLY_8_e2_1711_e7_1962
+FIREFLY_9
+FIREFLY_9_e7_170_e3_3647
+FIREFLY_a3
+FIREFLY_a3_e1_3233
+FIREFLY_a3_e1_3233_e1_3123
+FIREFLY_a3_e1_3233_e2_2392
+FIREFLY_a3_e1_3233_e3_2970
+FIREFLY_a3_e1_3233_e7_906
+FIREFLY_a3_e2_2086_e1_3235
+FIREFLY_a3_e2_2086_e2_2689
+FIREFLY_a3_e2_2086_e3_2542
+FIREFLY_a3_e2_2086_e7_2614
+FIREFLY_a3_e2_2952
+FIREFLY_a3_e3_314_e1_1979
+FIREFLY_a3_e3_314_e2_2812
+FIREFLY_a3_e3_314_e4_897
+FIREFLY_all
+FIREFLY_all_e1_1207_e1_1201
+FIREFLY_all_e1_1207_e2_3220
+FIREFLY_all_e1_1207_e3_1928
+FIREFLY_all_e1_1207_e7_156
+FIREFLY_all_e1_3406
+FIREFLY_all_e2_2924_e1_768
+FIREFLY_all_e2_2924_e2_1767
+FIREFLY_all_e2_2924_e3_3946
+FIREFLY_all_e2_2924_e7_3371
+FIREFLY_all_e2_3678
+FIREFLY_all_e3_1600_e1_667
+FIREFLY_all_e3_1600_e2_676
+FIREFLY_all_e3_1600_e3_2055
+FIREFLY_all_e3_1600_e4_2415
+FIREFLY_all_e3_1600_e5_84
+FIREFLY_all_e3_1600_e7_1607
+FIREFLY_all_e3_3496
+FIREFLY_all_e7_1909
+FIREFLY_luke_1a
+FIREFLY_luke_1a_e2_284_e1_2924
+FIREFLY_luke_1a_e2_284_e2_2755
+FIREFLY_luke_1a_e2_284_e3_3091
+FIREFLY_luke_1a_e2_284_e7_998
+FIREFLY_luke_1a_e7_3042_e3_1213
+FIREFLY_luke_1b
+FIREFLY_luke_1b_e1_1139_e1_1565
+FIREFLY_luke_1b_e1_1139_e2_2893
+FIREFLY_luke_1b_e1_1139_e3_1839
+FIREFLY_luke_1b_e1_1691
+FIREFLY_luke_1b_e2_3049
+FIREFLY_luke_1b_e2_3049_e1_946
+FIREFLY_luke_1b_e2_3049_e2_698
+FIREFLY_luke_1b_e2_3049_e3_2697
+FIREFLY_luke_1b_e3_671
+FIREFLY_luke_1b_e3_671_e1_725
+FIREFLY_luke_1b_e3_671_e2_2131
+FIREFLY_luke_1b_e3_671_e3_941
+FIREFLY_luke_1b_e3_671_e4_147
+FIREFLY_luke_1b_e3_671_e5_1637
+FIREFLY_luke_1b_e3_671_e6_1974
+FIREFLY_luke_1b_e3_671_e7_1882
+FIREFLY_luke_1b_e7_2574
+FIREFLY_luke_1b_e7_3191
+FIREFLY_luke_1b_e7_3191_e1_1303
+FIREFLY_luke_1b_e7_3191_e2_1864
+FIREFLY_luke_1b_e7_3191_e3_1250
+FIREFLY_luke_1b_e7_3191_e7_2146
+FIREFLY_luke_1b_e7_3191_e8_2830
+FIREFLY_luke_2
+FIREFLY_luke_2_e2_1375_e1_418
+FIREFLY_luke_2_e7_1826_e8_126
+FIREFLY_luke_3
+FIREFLY_luke_3_e1_2217_e3_1200
+FIREFLY_luke_4
+FIREFLY_luke_4_e2_325
+FIREFLY_luke_5
+FIREFLY_luke_rt
+FIREFLY_luke_rt_e1_913
+FIREFLY_luke_rt_e1_913_e1_1993
+FIREFLY_luke_rt_e1_913_e2_3353
+FIREFLY_luke_rt_e1_913_e3_2128
+FIREFLY_luke_rt_e1_913_e7_1403
+FIREFLY_luke_rt_e2_3460
+FIREFLY_luke_rt_e2_3460_e1_1455
+FIREFLY_luke_rt_e2_3460_e2_2670
+FIREFLY_luke_rt_e2_3460_e3_1333
+FIREFLY_luke_rt_e2_3460_e7_471
+FIREFLY_luke_rt_e3_1549
+FIREFLY_rt
+FIREFLY_rt_e3_1770_e2_637
+FIREFLY_u1
+FIREFLY_u1_e2_3403_e2_957
+FIREFLY_u1_e7_3318
+Gas
+ILLINOIS_1
+ILLINOIS_2
+ILLINOIS_2_e1_834
+ILLINOIS_2_e1_834_e1_1895
+ILLINOIS_2_e1_834_e2_3395
+ILLINOIS_2_e1_834_e3_2931
+ILLINOIS_2_e1_834_e7_3738
+ILLINOIS_2_e2_2367_e1_3182
+ILLINOIS_2_e2_2367_e2_1561
+ILLINOIS_2_e2_2367_e3_1601
+ILLINOIS_2_e2_2367_e7_2728
+ILLINOIS_2_e2_876
+ILLINOIS_3
+ILLINOIS_3_e3_2581
+ILLINOIS_3_e3_2581_e1_1130
+ILLINOIS_3_e3_2581_e2_2545
+ILLINOIS_3_e3_2581_e3_979
+ILLINOIS_3_e3_2581_e4_958
+ILLINOIS_3_e3_2581_e5_4006
+ILLINOIS_3_e3_2581_e7_3447
+ILLINOIS_4
+ILLINOIS_4_e7_2651_e7_2847
+ILLINOIS_5
+ILLINOIS_5_e7_692_e7_2865
+ILLINOIS_a1
+ILLINOIS_all
+ILLINOIS_r4a
+MESI_1_e2_162_e7_1545
+MESI_3_e2_819
+MESI_3_e2_819_e2_562
+MESI_3_e2_819_e3_2698
+MESI_3_e2_819_e5_2554
+MESI_3_e2_819_e7_1665
+MESI_3_e2_819_e8_1896
+MESI_4_e7_1140_e7_433
+MESI_all_e4_1147_e7_497
+MESI_i1
+MESI_i1_e2_1758_e8_12
+MESI_i1_e2_2656
+MESI_i1_e3_2145
+MESI_i1_e3_2145_e1_2667
+MESI_i1_e3_2145_e2_2228
+MESI_i1_e3_2145_e3_977
+MESI_i1_e3_2145_e4_1717
+MESI_i1_e3_2145_e5_2391
+MESI_i1_e3_2145_e7_1847
+MESI_i1_e3_2145_e8_2325
+MESI_i1_e4_1986
+MESI_i1_e4_1986_e1_1519
+MESI_i2
+MESI_i3
+MESI_i3_e1_447
+MESI_i3_e1_447_e1_1292
+MESI_i3_e1_447_e2_1098
+MESI_i3_e1_447_e3_1180
+MESI_i3_e1_447_e5_2444
+MESI_i3_e1_447_e6_2281
+MESI_i3_e1_447_e7_2194
+MESI_i4
+MESI_i4_e4_1689
+MESI_i4_e6_2175
+MESI_i4_e7_1017_e6_1132
+MESI_i4_e8_1381_e1_1837
+MESI_i4_e8_1381_e4_313
+MOESI_1_e2_982_e7_492
+MOESI_1_e3_1884_e7_1875
+MOESI_2_e1_1753_e1_1510
+MOESI_2_e1_1753_e2_615
+MOESI_2_e1_1753_e3_2021
+MOESI_2_e2_1599_e1_2383
+MOESI_2_e2_1599_e2_1815
+MOESI_2_e2_1599_e3_1658
+MOESI_2_e3_929_e1_2319
+MOESI_2_e3_929_e2_2421
+MOESI_2_e3_929_e3_2294
+MOESI_2_e3_929_e7_619
+MOESI_2_e7_2607
+MOESI_2_e7_2910
+MOESI_2_e7_2910_e1_1021
+MOESI_2_e7_2910_e2_611
+MOESI_2_e7_2910_e3_2002
+MOESI_2_e7_2910_e7_1804
+MOESI_2_e8_926_e7_961
+MOESI_all_e3_2032_e3_2788
+PRODUCER_CONSUMER_vt
+PRODUCER_CONSUMER_vt_e2_1352
+PRODUCER_CONSUMER_vt_e3_507
+PRODUCER_CONSUMER_vt_e7_1059_e8_1111
+PRODUCER_CONSUMMER_luke_1
+PRODUCER_CONSUMMER_luke_2
+PRODUCER_CONSUMMER_luke_2_e7_1068_e8_1019
+SYNAPSE_123_e2_1653
+SYNAPSE_123_e3_302
+SYNAPSE_123_e3_302_e1_1141
+SYNAPSE_123_e7_837_e2_1394
+SYNAPSE_123_e7_837_e3_135
+SYNAPSE_123_e7_837_e7_1262
+SYNAPSE_123_e7_856
+SYNAPSE_123_e8_953_e1_1128
+SYNAPSE_123_e8_953_e2_458
+SYNAPSE_123_e8_953_e3_271
+SYNAPSE_123_e8_953_e7_1465
+SYNAPSE_2_e1_1239
+SYNAPSE_2_e1_1239_e1_1331
+SYNAPSE_2_e1_1239_e2_74
+SYNAPSE_2_e3_216
+SYNAPSE_2_e8_1118_e1_667
+SYNAPSE_2_e8_1118_e2_237
+SYNAPSE_2_e8_1118_e3_1216
+SYNAPSE_3_e1_1416
+SYNAPSE_3_e1_1416_e1_1675
+SYNAPSE_3_e1_1416_e2_753
+SYNAPSE_3_e1_1416_e3_1191
+SYNAPSE_3_e1_1416_e7_193
+SYNAPSE_3_e3_1041
+SYNAPSE_3_e7_1444_e7_638
+SYNAPSE_3_e7_425
+SYNAPSE_3_e8_1329_e1_1270
+SYNAPSE_3_e8_1329_e2_236
+SYNAPSE_3_e8_1329_e3_421
+SYNAPSE_3_e8_1329_e7_1062
+SYNAPSE_5
+SYNAPSE_5_e1_811
+SYNAPSE_5_e1_811_e1_823
+SYNAPSE_5_e1_811_e2_1026
+SYNAPSE_5_e2_1525
+SYNAPSE_6
+SYNAPSE_6_e2_1439_e1_954
+SYNAPSE_6_e3_1666_e5_1558
+SYNAPSE_6_e7_938_e2_1012
+SYNAPSE_6_e8_1147_e2_1326
+SYNAPSE_all_e3_1750
+SYNAPSE_all_e3_1864_e3_495
+SYNAPSE_all_e3_1864_e4_34
+SYNAPSE_all_e3_1864_e5_1637
+SYNAPSE_all_e3_1864_e7_251
+SYNAPSE_all_e7_907
+SYNAPSE_all_e7_907_e7_1363
+SYNAPSE_all_e8_251_e1_1852
+SYNAPSE_all_e8_251_e2_1053
+SYNAPSE_all_e8_251_e3_1472
+SYNAPSE_i1
+_6counter
+_6counter2
+_6countern
+_6counters
+_6counters_e3_140_e8_149
+_6counters_e8_371_e1_448
+_6counters_e8_371_e3_224
+_6counters_e8_371_e7_304
+car_1_e7_184_e3_299
+car_2_e7_1027_e1_1047
+car_2_e7_1027_e7_359
+car_2_e8_491_e7_826
+car_3_e1_586
+car_3_e1_924
+car_3_e7_626_e1_305
+car_3_e8_33_e1_856
+car_4_e3_556
+car_4_e3_57
+car_4_e3_57_e5_999
+car_4_e7_592_e3_442
+car_4_e7_592_e7_265
+car_4_e8_118_e3_514
+car_4_e8_118_e7_178
+car_5
+car_5_e2_405_e2_1083
+car_5_e2_405_e3_473
+car_5_e2_405_e8_1055
+car_5_e3_11_e1_429
+car_5_e3_11_e5_24
+car_5_e3_661
+car_5_e7_244
+car_5_e7_244_e1_823
+car_5_e7_244_e2_693
+car_5_e7_244_e3_1071
+car_6
+car_6_e1_152
+car_6_e1_152_e1_391
+car_6_e2_589_e2_506
+car_6_e2_589_e3_349
+car_6_e2_893
+car_6_e3_294_e1_956
+car_6_e3_294_e3_47
+car_6_e3_294_e5_979
+car_all_e1_618
+car_all_e1_618_e3_303
+car_all_e2_142_e7_209
+car_all_e3_1068
+car_all_e3_1068_e1_178
+car_all_e3_1068_e2_13
+car_all_e3_1068_e3_163
+car_all_e3_1068_e5_882
+car_all_e7_188_e7_743
+car_all_e8_856_e1_217
+car_all_e8_856_e3_180
+car_all_e8_856_e7_578
+ccp08
+ccp10
+ccp11
+ccp12
+ccp13
+ccp14
+ccp17
+ccp18
+ccp20
+ccp21
+ccp22
+ccp23
+ccp24
+cd_e7_621_e7_669
+cd_e7_8
+cruise_controller_08
+cruise_controller_09
+cruise_controller_10
+cruise_controller_12
+cruise_controller_14
+cruise_controller_15
+cruise_controller_16
+cruise_controller_17
+cruise_controller_18
+cruise_controller_19
+cruise_controller_20
+cruise_controller_21
+cruise_controller_22
+cruise_controller_23
+cruise_controller_24
+durationThm_1
+durationThm_1_e1_350
+durationThm_1_e3_389
+durationThm_1_e3_389_e5_5
+durationThm_1_e7_217
+durationThm_1_e7_217_e1_89
+durationThm_1_e7_217_e3_132
+durationThm_1_e7_217_e7_31
+durationThm_2
+durationThm_2_e1_301
+durationThm_2_e3_329_e5_124
+durationThm_2_e3_99
+durationThm_2_e7_145_e1_343
+durationThm_2_e7_145_e3_222
+durationThm_2_e7_145_e7_154
+durationThm_2_e7_145_e8_73
+durationThm_2_e7_149
+durationThm_3
+durationThm_3_e1_36
+durationThm_3_e1_71
+durationThm_3_e7_334
+durationThm_3_e7_334_e1_431
+durationThm_3_e7_334_e3_42
+durationThm_3_e7_334_e7_118
+ex8_e7_74
+ex8_e7_74_e7_740
+ex8_e7_74_e8_302
+ex8_e8_220
+ex8_e8_220_e7_249
+ex8_e8_376
+fast_1_e7_2044
+fast_1_e7_2044_e7_1287
+fast_1_e8_747_e7_692
+fast_2_e7_2526
+fast_2_e7_2526_e7_2736
+fast_2_e8_460_e7_43
+metros_2
+metros_2_e1_1116
+metros_2_e1_1116_e1_556
+metros_2_e1_1116_e3_287
+metros_2_e1_1116_e7_1440
+metros_2_e1_190
+metros_2_e2_704_e1_389
+metros_2_e2_704_e3_76
+metros_2_e2_704_e7_810
+metros_2_e2_968
+metros_2_e3_112
+metros_3
+metros_3_e3_1275
+metros_3_e3_1275_e1_1350
+metros_3_e3_1275_e4_164
+metros_3_e3_1275_e5_846
+metros_3_e3_1275_e6_1315
+metros_3_e3_1275_e7_529
+metros_3_e4_987
+metros_3_e4_987_e2_80
+metros_3_e4_987_e3_291
+metros_4
+metros_4_e1_821_e5_911
+metros_4_e1_917
+metros_4_e2_968
+metros_4_e2_968_e1_956
+metros_4_e2_968_e4_801
+metros_4_e2_968_e5_991
+metros_4_e2_968_e6_236
+metros_4_e2_968_e7_860
+metros_4_e3_1025
+metros_4_e3_1091
+metros_4_e3_1091_e1_1044
+metros_4_e3_1091_e4_232
+metros_4_e5_1150
+metros_4_e6_239_e2_307
+metros_5
+metros_5_e4_1208_e1_337
+microwave06
+microwave07
+microwave08
+microwave09
+microwave10
+microwave11
+microwave12
+microwave13
+microwave14
+microwave17
+microwave18
+microwave19
+microwave20
+microwave21
+microwave22
+microwave23
+microwave24
+microwave25
+microwave27
+microwave28
+microwave30
+microwave31
+microwave32
+microwave33
+microwave34
+microwave35
+microwave36
+microwave37
+microwave38
+microwave39
+microwave40
+peterson_1
+peterson_1_e7_4234
+peterson_2
+peterson_3
+peterson_4
+peterson_all
+peterson_vt
+readwrit
+rtp_1
+rtp_10
+rtp_10_e7_106_e7_2564
+rtp_2
+rtp_3
+rtp_4
+rtp_5
+rtp_5_e7_3972
+rtp_6
+rtp_7
+rtp_8
+rtp_9
+rtp_all
+rtp_all_e7_2500
+rtp_vt
+stalmark_e8_48
+stalmark_e8_64
+stalmark_e8_64_e7_80
+stalmark_e8_64_e8_207
+swimmingpool_1
+swimmingpool_1_e7_1621
+swimmingpool_2
+swimmingpool_3
+swimmingpool_4
+swimmingpool_4_e7_2197
+swimmingpool_5
+swimmingpool_6
+swimmingpool_6_e7_10_e7_341
+swimmingpool_6_e7_399
+swimmingpool_7
+swimmingpool_8
+swimmingpool_9
+switch
+switch2
+ticket3i_1
+ticket3i_1_e7_1669
+ticket3i_2
+ticket3i_3
+ticket3i_3_e7_1312
+ticket3i_3_e7_1312_e7_1495
+ticket3i_3_e7_1312_e8_1916
+ticket3i_3_e7_99
+ticket3i_3_e8_1703
+ticket3i_3_e8_1703_e7_3491
+ticket3i_3_e8_1703_e8_2560
+ticket3i_3_e8_1788
+ticket3i_4
+ticket3i_4_e7_1775_e7_3320
+ticket3i_5
+ticket3i_5_e7_3307
+ticket3i_6
+ticket3i_6_e7_1096_e7_2688
+ticket3i_7
+ticket3i_7_e1_2192_e1_1852
+ticket3i_7_e2_2724_e7_524
+ticket3i_7_e3_59_e7_2122
+ticket3i_7_e7_3176
+ticket3i_7_e7_3176_e1_2924
+ticket3i_7_e8_2126_e7_78
+ticket3i_all
+ticket3i_all_e1_2706_e7_1776
+ticket3i_all_e2_1117_e7_553
+ticket3i_all_e3_557_e7_3464
+ticket3i_all_e7_1837
+ticket3i_all_e7_591
+ticket3i_all_e8_505_e7_2450
+traffic_e7_46
+traffic_e7_46_e7_171
+twisted_counters
+two_counters_e1_268
+two_counters_e2_3
+two_counters_e3_325
+two_counters_e7_222
+ums_e7_1700
diff --git a/offline_tests/metros_1.lus b/offline_tests/metros_1.lus
index 80d577e5..41f972be 100644
--- a/offline_tests/metros_1.lus
+++ b/offline_tests/metros_1.lus
@@ -46,7 +46,7 @@ tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e1_846_e1_1317.lus b/offline_tests/metros_1_e1_846_e1_1317.lus
index 48bee70f..c6a13c06 100644
--- a/offline_tests/metros_1_e1_846_e1_1317.lus
+++ b/offline_tests/metros_1_e1_846_e1_1317.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e1_846_e2_1394.lus b/offline_tests/metros_1_e1_846_e2_1394.lus
index 78d61fe8..66c7b8a4 100644
--- a/offline_tests/metros_1_e1_846_e2_1394.lus
+++ b/offline_tests/metros_1_e1_846_e2_1394.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e1_846_e3_1060.lus b/offline_tests/metros_1_e1_846_e3_1060.lus
index c5483b33..8d571bbc 100644
--- a/offline_tests/metros_1_e1_846_e3_1060.lus
+++ b/offline_tests/metros_1_e1_846_e3_1060.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e1_846_e7_397.lus b/offline_tests/metros_1_e1_846_e7_397.lus
index 035e9424..edfda059 100644
--- a/offline_tests/metros_1_e1_846_e7_397.lus
+++ b/offline_tests/metros_1_e1_846_e7_397.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e2_1102_e1_317.lus b/offline_tests/metros_1_e2_1102_e1_317.lus
index 00a46455..ea437fea 100644
--- a/offline_tests/metros_1_e2_1102_e1_317.lus
+++ b/offline_tests/metros_1_e2_1102_e1_317.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e2_1102_e2_943.lus b/offline_tests/metros_1_e2_1102_e2_943.lus
index 3ffca1fb..837d0e1e 100644
--- a/offline_tests/metros_1_e2_1102_e2_943.lus
+++ b/offline_tests/metros_1_e2_1102_e2_943.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e2_1102_e3_961.lus b/offline_tests/metros_1_e2_1102_e3_961.lus
index 26bec51f..abe4e2ea 100644
--- a/offline_tests/metros_1_e2_1102_e3_961.lus
+++ b/offline_tests/metros_1_e2_1102_e3_961.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e2_1102_e7_1163.lus b/offline_tests/metros_1_e2_1102_e7_1163.lus
index b6d02122..a06dc573 100644
--- a/offline_tests/metros_1_e2_1102_e7_1163.lus
+++ b/offline_tests/metros_1_e2_1102_e7_1163.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e2_627.lus b/offline_tests/metros_1_e2_627.lus
index e29631b8..cca69555 100644
--- a/offline_tests/metros_1_e2_627.lus
+++ b/offline_tests/metros_1_e2_627.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e7_1255_e7_12.lus b/offline_tests/metros_1_e7_1255_e7_12.lus
index d390eb1c..a950e14d 100644
--- a/offline_tests/metros_1_e7_1255_e7_12.lus
+++ b/offline_tests/metros_1_e7_1255_e7_12.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e7_606.lus b/offline_tests/metros_1_e7_606.lus
index 0c0cbf32..fc7d050b 100644
--- a/offline_tests/metros_1_e7_606.lus
+++ b/offline_tests/metros_1_e7_606.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e8_725.lus b/offline_tests/metros_1_e8_725.lus
index 8a7c713c..7fda7aac 100644
--- a/offline_tests/metros_1_e8_725.lus
+++ b/offline_tests/metros_1_e8_725.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e8_725_e1_919.lus b/offline_tests/metros_1_e8_725_e1_919.lus
index 8cf00463..dd3fdd4f 100644
--- a/offline_tests/metros_1_e8_725_e1_919.lus
+++ b/offline_tests/metros_1_e8_725_e1_919.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e8_725_e2_1144.lus b/offline_tests/metros_1_e8_725_e2_1144.lus
index 14f55753..5b28df89 100644
--- a/offline_tests/metros_1_e8_725_e2_1144.lus
+++ b/offline_tests/metros_1_e8_725_e2_1144.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_1_e8_725_e3_556.lus b/offline_tests/metros_1_e8_725_e3_556.lus
index 9a3f5acf..a2a55716 100644
--- a/offline_tests/metros_1_e8_725_e3_556.lus
+++ b/offline_tests/metros_1_e8_725_e3_556.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var nB0, nB1 : int;
nS : int;
diff0, diff1 :int;
diff --git a/offline_tests/metros_2_e1_1116_e2_617.lus b/offline_tests/metros_2_e1_1116_e2_617.lus
index 4574dca5..e82e9f80 100644
--- a/offline_tests/metros_2_e1_1116_e2_617.lus
+++ b/offline_tests/metros_2_e1_1116_e2_617.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0, nB1 : int;
nS : int;
diff0,diff1:int;
diff --git a/offline_tests/metros_2_e2_704_e2_13.lus b/offline_tests/metros_2_e2_704_e2_13.lus
index 3d98232d..a0df140a 100644
--- a/offline_tests/metros_2_e2_704_e2_13.lus
+++ b/offline_tests/metros_2_e2_704_e2_13.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0, nB1 : int;
nS : int;
diff0,diff1:int;
diff --git a/offline_tests/metros_3_e3_1275_e2_454.lus b/offline_tests/metros_3_e3_1275_e2_454.lus
index 23b7c3ef..6db4ffbb 100644
--- a/offline_tests/metros_3_e3_1275_e2_454.lus
+++ b/offline_tests/metros_3_e3_1275_e2_454.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0,nB1 : int;
nS : int;
diff0,diff1:int;
diff --git a/offline_tests/metros_3_e3_1275_e3_640.lus b/offline_tests/metros_3_e3_1275_e3_640.lus
index 05e2cc6c..f153e8ef 100644
--- a/offline_tests/metros_3_e3_1275_e3_640.lus
+++ b/offline_tests/metros_3_e3_1275_e3_640.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0, B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0,nB1 : int;
nS : int;
diff0,diff1:int;
diff --git a/offline_tests/metros_4_e2_968_e2_1166.lus b/offline_tests/metros_4_e2_968_e2_1166.lus
index f9b45f04..e0a5a289 100644
--- a/offline_tests/metros_4_e2_968_e2_1166.lus
+++ b/offline_tests/metros_4_e2_968_e2_1166.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0,B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0,nB1 : int;
nS : int;
diff0,diff1:int;
diff --git a/offline_tests/metros_4_e2_968_e3_931.lus b/offline_tests/metros_4_e2_968_e3_931.lus
index 3143486c..5bde5408 100644
--- a/offline_tests/metros_4_e2_968_e3_931.lus
+++ b/offline_tests/metros_4_e2_968_e3_931.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0,B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0,nB1 : int;
nS : int;
diff0,diff1:int;
diff --git a/offline_tests/metros_4_e3_1091_e2_1317.lus b/offline_tests/metros_4_e3_1091_e2_1317.lus
index 927fb422..3ac8b39b 100644
--- a/offline_tests/metros_4_e3_1091_e2_1317.lus
+++ b/offline_tests/metros_4_e3_1091_e2_1317.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0,B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0,nB1 : int;
nS : int;
diff0,diff1:int;
diff --git a/offline_tests/metros_4_e3_1091_e3_522.lus b/offline_tests/metros_4_e3_1091_e3_522.lus
index 0011d234..c6ccf1ed 100644
--- a/offline_tests/metros_4_e3_1091_e3_522.lus
+++ b/offline_tests/metros_4_e3_1091_e3_522.lus
@@ -40,7 +40,7 @@ let
tel
node top(B0,B1 : bool; S : bool)
returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var nB0,nB1 : int;
nS : int;
diff0,diff1:int;
diff --git a/offline_tests/microwave01.lus b/offline_tests/microwave01.lus
index 2976a5d4..c6ed6fe5 100644
--- a/offline_tests/microwave01.lus
+++ b/offline_tests/microwave01.lus
@@ -14,7 +14,7 @@ node top(KP_START: bool;
) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
LEFT_DIGIT: int;
SETUP: bool;
diff --git a/offline_tests/microwave02.lus b/offline_tests/microwave02.lus
index 40270311..a3c31a94 100644
--- a/offline_tests/microwave02.lus
+++ b/offline_tests/microwave02.lus
@@ -14,7 +14,7 @@ node top(KP_START: bool;
) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
LEFT_DIGIT: int;
SETUP: bool;
diff --git a/offline_tests/microwave03.lus b/offline_tests/microwave03.lus
index 1c6797ec..552baf18 100644
--- a/offline_tests/microwave03.lus
+++ b/offline_tests/microwave03.lus
@@ -14,7 +14,7 @@ node top(KP_START: bool;
) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
LEFT_DIGIT: int;
SETUP: bool;
diff --git a/offline_tests/microwave04.lus b/offline_tests/microwave04.lus
index e965affd..5a0720e5 100644
--- a/offline_tests/microwave04.lus
+++ b/offline_tests/microwave04.lus
@@ -14,7 +14,7 @@ node top(KP_START: bool;
) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
LEFT_DIGIT: int;
SETUP: bool;
diff --git a/offline_tests/microwave05.lus b/offline_tests/microwave05.lus
index 6d38c766..5b88b1b5 100644
--- a/offline_tests/microwave05.lus
+++ b/offline_tests/microwave05.lus
@@ -14,7 +14,7 @@ node top(KP_START: bool;
) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 25-induction;
var
LEFT_DIGIT: int;
SETUP: bool;
diff --git a/offline_tests/microwave15.lus b/offline_tests/microwave15.lus
index 7a915ee9..a3ab42af 100644
--- a/offline_tests/microwave15.lus
+++ b/offline_tests/microwave15.lus
@@ -14,7 +14,7 @@ node top(KP_START: bool;
) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
LEFT_DIGIT: int;
SETUP: bool;
diff --git a/offline_tests/microwave16.lus b/offline_tests/microwave16.lus
index 6d52e9a6..7fbd2152 100644
--- a/offline_tests/microwave16.lus
+++ b/offline_tests/microwave16.lus
@@ -14,7 +14,7 @@ node top(KP_START: bool;
) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var
LEFT_DIGIT: int;
SETUP: bool;
diff --git a/offline_tests/peterson_1.lus b/offline_tests/peterson_1.lus
index 9db23a52..3d9c3603 100644
--- a/offline_tests/peterson_1.lus
+++ b/offline_tests/peterson_1.lus
@@ -121,7 +121,7 @@ tel
node top(e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool)
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13 : int;
env : bool;
let
diff --git a/offline_tests/peterson_2.lus b/offline_tests/peterson_2.lus
index 0809775e..f8cd8460 100644
--- a/offline_tests/peterson_2.lus
+++ b/offline_tests/peterson_2.lus
@@ -121,7 +121,7 @@ tel
node top(e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool)
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13 : int;
env : bool;
let
diff --git a/offline_tests/peterson_3.lus b/offline_tests/peterson_3.lus
index 09b8f74c..688e0f77 100644
--- a/offline_tests/peterson_3.lus
+++ b/offline_tests/peterson_3.lus
@@ -121,7 +121,7 @@ tel
node top(e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool)
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13 : int;
env : bool;
let
diff --git a/offline_tests/peterson_4.lus b/offline_tests/peterson_4.lus
index aced6216..fce518bf 100644
--- a/offline_tests/peterson_4.lus
+++ b/offline_tests/peterson_4.lus
@@ -121,7 +121,7 @@ tel
node top(e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool)
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13 : int;
env : bool;
let
diff --git a/offline_tests/peterson_all.lus b/offline_tests/peterson_all.lus
index 75ef951b..ec996d39 100644
--- a/offline_tests/peterson_all.lus
+++ b/offline_tests/peterson_all.lus
@@ -121,7 +121,7 @@ tel
node top(e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool)
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13 : int;
env : bool;
let
diff --git a/offline_tests/readwrit.lus b/offline_tests/readwrit.lus
index 14fe29df..0f6c45f0 100644
--- a/offline_tests/readwrit.lus
+++ b/offline_tests/readwrit.lus
@@ -109,7 +109,7 @@ tel
node top(etat1, etat2, etat3, etat4, etat5, etat6, etat7, etat8, etat9 : bool)
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12 : int;
env : bool;
let
diff --git a/offline_tests/rtp_1.lus b/offline_tests/rtp_1.lus
index e81e71bb..71461444 100644
--- a/offline_tests/rtp_1.lus
+++ b/offline_tests/rtp_1.lus
@@ -97,7 +97,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var X1, X2, X3, X4, X5, X6, X7, X8, X9 : int;
erreur : bool;
let
diff --git a/offline_tests/rtp_10.lus b/offline_tests/rtp_10.lus
index e176eb30..7e7c7693 100644
--- a/offline_tests/rtp_10.lus
+++ b/offline_tests/rtp_10.lus
@@ -97,7 +97,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var X1, X2, X3, X4, X5, X6, X7, X8, X9 : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/rtp_2.lus b/offline_tests/rtp_2.lus
index 42ba8ee0..99d54f78 100644
--- a/offline_tests/rtp_2.lus
+++ b/offline_tests/rtp_2.lus
@@ -97,7 +97,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var X1, X2, X3, X4, X5, X6, X7, X8, X9 : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/rtp_3.lus b/offline_tests/rtp_3.lus
index 4589bb27..83b11f2a 100644
--- a/offline_tests/rtp_3.lus
+++ b/offline_tests/rtp_3.lus
@@ -97,7 +97,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var X1, X2, X3, X4, X5, X6, X7, X8, X9 : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/rtp_4.lus b/offline_tests/rtp_4.lus
index b2aaa8ca..c60e8df3 100644
--- a/offline_tests/rtp_4.lus
+++ b/offline_tests/rtp_4.lus
@@ -97,7 +97,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var X1, X2, X3, X4, X5, X6, X7, X8, X9 : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/rtp_5.lus b/offline_tests/rtp_5.lus
index af6ecb24..51511bf0 100644
--- a/offline_tests/rtp_5.lus
+++ b/offline_tests/rtp_5.lus
@@ -97,7 +97,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var X1, X2, X3, X4, X5, X6, X7, X8, X9 : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/rtp_6.lus b/offline_tests/rtp_6.lus
index aec94646..3b164f82 100644
--- a/offline_tests/rtp_6.lus
+++ b/offline_tests/rtp_6.lus
@@ -97,7 +97,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var X1, X2, X3, X4, X5, X6, X7, X8, X9 : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/rtp_7.lus b/offline_tests/rtp_7.lus
index 4b288e5a..914f501d 100644
--- a/offline_tests/rtp_7.lus
+++ b/offline_tests/rtp_7.lus
@@ -97,7 +97,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var X1, X2, X3, X4, X5, X6, X7, X8, X9 : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/rtp_8.lus b/offline_tests/rtp_8.lus
index 2e890742..40ba06ea 100644
--- a/offline_tests/rtp_8.lus
+++ b/offline_tests/rtp_8.lus
@@ -97,7 +97,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var X1, X2, X3, X4, X5, X6, X7, X8, X9 : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/rtp_9.lus b/offline_tests/rtp_9.lus
index 498fecbd..aaf814b2 100644
--- a/offline_tests/rtp_9.lus
+++ b/offline_tests/rtp_9.lus
@@ -97,7 +97,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var X1, X2, X3, X4, X5, X6, X7, X8, X9 : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/rtp_all.lus b/offline_tests/rtp_all.lus
index 45566ba4..3d3c507c 100644
--- a/offline_tests/rtp_all.lus
+++ b/offline_tests/rtp_all.lus
@@ -97,7 +97,7 @@ tel
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var X1, X2, X3, X4, X5, X6, X7, X8, X9 : int;
erreur : bool;
env : bool;
diff --git a/offline_tests/speed2.lus b/offline_tests/speed2.lus
index fce86d47..2d9aa5cc 100644
--- a/offline_tests/speed2.lus
+++ b/offline_tests/speed2.lus
@@ -23,7 +23,7 @@ let
tel
--subrange [0, 2] of int
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var late,early: bool;
let
(late,early) = speed(beacon,second);
diff --git a/offline_tests/speed2_e7_223_e7_213.lus b/offline_tests/speed2_e7_223_e7_213.lus
index 8a9d5d0e..3420216c 100644
--- a/offline_tests/speed2_e7_223_e7_213.lus
+++ b/offline_tests/speed2_e7_223_e7_213.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var late,early: bool;
let
(late,early) = speed(beacon,second);
diff --git a/offline_tests/speed2_e7_223_e8_329.lus b/offline_tests/speed2_e7_223_e8_329.lus
index bf091859..e291c2ed 100644
--- a/offline_tests/speed2_e7_223_e8_329.lus
+++ b/offline_tests/speed2_e7_223_e8_329.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var late,early: bool;
let
(late,early) = speed(beacon,second);
diff --git a/offline_tests/speed2_e7_496.lus b/offline_tests/speed2_e7_496.lus
index 4c53edb8..9411f057 100644
--- a/offline_tests/speed2_e7_496.lus
+++ b/offline_tests/speed2_e7_496.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var late,early: bool;
let
(late,early) = speed(beacon,second);
diff --git a/offline_tests/speed2_e8_449.lus b/offline_tests/speed2_e8_449.lus
index 3f71579c..37a00e2d 100644
--- a/offline_tests/speed2_e8_449.lus
+++ b/offline_tests/speed2_e8_449.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var late,early: bool;
let
(late,early) = speed(beacon,second);
diff --git a/offline_tests/speed2_e8_449_e7_353.lus b/offline_tests/speed2_e8_449_e7_353.lus
index 29bb5258..84a354ed 100644
--- a/offline_tests/speed2_e8_449_e7_353.lus
+++ b/offline_tests/speed2_e8_449_e7_353.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var late,early: bool;
let
(late,early) = speed(beacon,second);
diff --git a/offline_tests/speed2_e8_449_e8_517.lus b/offline_tests/speed2_e8_449_e8_517.lus
index 6252de12..3e7c7b70 100644
--- a/offline_tests/speed2_e8_449_e8_517.lus
+++ b/offline_tests/speed2_e8_449_e8_517.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 3-induction;
var late,early: bool;
let
(late,early) = speed(beacon,second);
diff --git a/offline_tests/speed2_e8_750.lus b/offline_tests/speed2_e8_750.lus
index 3f71579c..37a00e2d 100644
--- a/offline_tests/speed2_e8_750.lus
+++ b/offline_tests/speed2_e8_750.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var late,early: bool;
let
(late,early) = speed(beacon,second);
diff --git a/offline_tests/speed_e7_207.lus b/offline_tests/speed_e7_207.lus
index f906c026..050a8dec 100644
--- a/offline_tests/speed_e7_207.lus
+++ b/offline_tests/speed_e7_207.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var late,early: bool;
let
OK = not (late and early);
diff --git a/offline_tests/speed_e7_207_e7_538.lus b/offline_tests/speed_e7_207_e7_538.lus
index 60ba0c85..8e4de02a 100644
--- a/offline_tests/speed_e7_207_e7_538.lus
+++ b/offline_tests/speed_e7_207_e7_538.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var late,early: bool;
let
OK = not (late and early);
diff --git a/offline_tests/speed_e7_207_e8_507.lus b/offline_tests/speed_e7_207_e8_507.lus
index cb9c81ff..d3c6d238 100644
--- a/offline_tests/speed_e7_207_e8_507.lus
+++ b/offline_tests/speed_e7_207_e8_507.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var late,early: bool;
let
OK = not (late and early);
diff --git a/offline_tests/speed_e7_492.lus b/offline_tests/speed_e7_492.lus
index f906c026..050a8dec 100644
--- a/offline_tests/speed_e7_492.lus
+++ b/offline_tests/speed_e7_492.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var late,early: bool;
let
OK = not (late and early);
diff --git a/offline_tests/speed_e8_649.lus b/offline_tests/speed_e8_649.lus
index ed11ce89..119e6c19 100644
--- a/offline_tests/speed_e8_649.lus
+++ b/offline_tests/speed_e8_649.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var late,early: bool;
let
OK = not (late and early);
diff --git a/offline_tests/speed_e8_649_e7_709.lus b/offline_tests/speed_e8_649_e7_709.lus
index ace6d99e..7d951c8e 100644
--- a/offline_tests/speed_e8_649_e7_709.lus
+++ b/offline_tests/speed_e8_649_e7_709.lus
@@ -20,7 +20,7 @@ let
else (diff <= -10);
tel
node top(beacon,second:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 1-induction;
var late,early: bool;
let
OK = not (late and early);
diff --git a/offline_tests/stalmark.lus b/offline_tests/stalmark.lus
index 1f066a13..80d9f13e 100644
--- a/offline_tests/stalmark.lus
+++ b/offline_tests/stalmark.lus
@@ -1,5 +1,5 @@
node top (x:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var a,b,c:bool;
let
a = true -> pre(c);
diff --git a/offline_tests/stalmark_e7_27.lus b/offline_tests/stalmark_e7_27.lus
index bf49288d..091d6a16 100644
--- a/offline_tests/stalmark_e7_27.lus
+++ b/offline_tests/stalmark_e7_27.lus
@@ -1,5 +1,5 @@
node top (x:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 4-induction;
var a,b,c:bool;
let
a = true -> pre(c);
diff --git a/offline_tests/stalmark_e7_27_e7_31.lus b/offline_tests/stalmark_e7_27_e7_31.lus
index 527d29bf..4c2b21f4 100644
--- a/offline_tests/stalmark_e7_27_e7_31.lus
+++ b/offline_tests/stalmark_e7_27_e7_31.lus
@@ -1,5 +1,5 @@
node top (x:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 4-induction;
var a,b,c:bool;
let
a = true -> pre(c);
diff --git a/offline_tests/stalmark_e7_76.lus b/offline_tests/stalmark_e7_76.lus
index 15a0e39d..b8a6698a 100644
--- a/offline_tests/stalmark_e7_76.lus
+++ b/offline_tests/stalmark_e7_76.lus
@@ -1,5 +1,5 @@
node top (x:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 4-induction;
var a,b,c:bool;
let
a = true -> pre(c);
diff --git a/offline_tests/steam_boiler_no_arr2_e6_3003_e4_15091.lus b/offline_tests/steam_boiler_no_arr2_e6_3003_e4_15091.lus
index 8de28af6..7a0e2507 100644
--- a/offline_tests/steam_boiler_no_arr2_e6_3003_e4_15091.lus
+++ b/offline_tests/steam_boiler_no_arr2_e6_3003_e4_15091.lus
@@ -629,7 +629,7 @@ node top(
q:int;
pump_state_0,pump_state_1,pump_state_2,pump_state_3:int)
returns(OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
op_mode_ :int;
mode__normal_then_water_level_ok,
diff --git a/offline_tests/switch.lus b/offline_tests/switch.lus
index 934205f9..e63fa7c8 100644
--- a/offline_tests/switch.lus
+++ b/offline_tests/switch.lus
@@ -1,23 +1,23 @@
-node SWITCH1 (set,reset,initial:bool) returns (level:bool);
+node SWITCH1 (set,reset,init:bool) returns (level:bool);
let
- level = initial -> if set then true
- else if reset then false
- else pre(level);
+ level = init -> if set then true
+ else if reset then false
+ else pre(level);
tel
-node SWITCH (set,reset,initial:bool) returns (level:bool);
+node SWITCH (set,reset,init:bool) returns (level:bool);
let
- level = initial -> if set and not pre(level) then true
- else if reset then false
- else pre(level);
+ level = init -> if set and not pre(level) then true
+ else if reset then false
+ else pre(level);
tel
-node top(set, treset, initial:bool) returns (OK:bool);
+node top(set, treset, init:bool) returns (OK:bool);
--@ contract guarantee OK;
var level,level1:bool;
let
- level = SWITCH(set,treset,initial);
- level1 = SWITCH1(set,treset,initial);
+ level = SWITCH(set,treset,init);
+ level1 = SWITCH1(set,treset,init);
OK = if (not(set and treset)) then
(level = level1)
else true;
diff --git a/offline_tests/switch2.lus b/offline_tests/switch2.lus
index 8e6c0b02..88971703 100644
--- a/offline_tests/switch2.lus
+++ b/offline_tests/switch2.lus
@@ -1,24 +1,24 @@
-node SWITCH1 (set,reset,initial:bool) returns (level:bool);
+node SWITCH1 (set,reset,init:bool) returns (level:bool);
let
- level = initial -> if set then true
- else if reset then false
- else pre(level);
+ level = init -> if set then true
+ else if reset then false
+ else pre(level);
tel
-node SWITCH (set,reset,initial:bool) returns (level:bool);
+node SWITCH (set,reset,init:bool) returns (level:bool);
let
- level = initial -> if set and not pre(level) then true
- else if reset then false
- else pre(level);
+ level = init -> if set and not pre(level) then true
+ else if reset then false
+ else pre(level);
tel
--requires assert to be true
-node top(set, treset, initial:bool) returns (OK:bool);
+node top(set, treset, init:bool) returns (OK:bool);
--@ contract guarantee OK;
var level,level1:bool;
let
- level = SWITCH(set,treset,initial);
- level1 = SWITCH1(set,treset,initial);
+ level = SWITCH(set,treset,init);
+ level1 = SWITCH1(set,treset,init);
OK = if not(set and treset) then(level = level1) else true;
-- assert not(set and treset);
--%PROPERTY OK=true;
diff --git a/offline_tests/test.ml b/offline_tests/test.ml
index 347b3759..de399d33 100644
--- a/offline_tests/test.ml
+++ b/offline_tests/test.ml
@@ -159,6 +159,7 @@ let config_format_tags =
let mark_open_stag = function
| String_tag "bold" -> "\x1b[1m"
| String_tag "red" -> "\x1b[31m"
+ | String_tag "magenta" -> "\x1b[35m"
| String_tag "green" -> "\x1b[32m"
| _ -> ""
in
@@ -287,7 +288,7 @@ let rec verify report timeout fs =
("KO" ^ if already then " (A)" else "\n" ^ read_whole_file err_f), fs
in
let tm r f : _ * _ * _ * _ format * _ * _ =
- r, ok, ko + 1, "@{<red>%s@}", "TO", f :: fs
+ r, ok, ko + 1, "@{<magenta>%s@}", "TO", f :: fs
in
let report, ok, ko, fmt_str, check, fs =
if is_verified report f' then success ~already:true report
@@ -343,8 +344,10 @@ let () =
in
let report = parse_report () in
let report = compile report lustrec lus_fs in
- print_ignored (List.map (fun f -> Filename.remove_extension f ^ ".c") ignored_fs);
+ print_ignored (List.map (fun f -> f ^ ".c") ignored_fs);
let lus_fs =
- List.(sort_uniq compare (filter (fun f -> not (mem f ignored_fs)) lus_fs))
+ List.(sort_uniq compare
+ (filter (fun f ->
+ not (mem (Filename.chop_extension f) ignored_fs)) lus_fs))
in
verify report (next_timeout report) lus_fs
diff --git a/offline_tests/ticket3i_1.lus b/offline_tests/ticket3i_1.lus
index 09e6d24b..0ab84126 100644
--- a/offline_tests/ticket3i_1.lus
+++ b/offline_tests/ticket3i_1.lus
@@ -84,7 +84,7 @@ tel
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
init_a1, init_a2, init_a3, init_t : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var p1, p2, p3, t, s, a1, a2, a3 : int;
erreur_ticket3i : bool;
let
diff --git a/offline_tests/ticket3i_2.lus b/offline_tests/ticket3i_2.lus
index d7a9b3eb..f374aa2c 100644
--- a/offline_tests/ticket3i_2.lus
+++ b/offline_tests/ticket3i_2.lus
@@ -85,7 +85,7 @@ tel
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
init_a1, init_a2, init_a3, init_t : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var p1, p2, p3, t, s, a1, a2, a3 : int;
erreur_ticket3i : bool;
env : bool;
diff --git a/offline_tests/ticket3i_3.lus b/offline_tests/ticket3i_3.lus
index 77a05fe9..df650502 100644
--- a/offline_tests/ticket3i_3.lus
+++ b/offline_tests/ticket3i_3.lus
@@ -85,7 +85,7 @@ tel
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
init_a1, init_a2, init_a3, init_t : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var p1, p2, p3, t, s, a1, a2, a3 : int;
erreur_ticket3i : bool;
env : bool;
diff --git a/offline_tests/ticket3i_3_e7_1312_e8_1916.lus b/offline_tests/ticket3i_3_e7_1312_e8_1916.lus
index f9551d56..be1def0a 100644
--- a/offline_tests/ticket3i_3_e7_1312_e8_1916.lus
+++ b/offline_tests/ticket3i_3_e7_1312_e8_1916.lus
@@ -70,7 +70,7 @@ tel
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
init_a1, init_a2, init_a3, init_t : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var p1, p2, p3, t, s, a1, a2, a3 : int;
erreur_ticket3i : bool;
env : bool;
diff --git a/offline_tests/ticket3i_3_e8_1703.lus b/offline_tests/ticket3i_3_e8_1703.lus
index 5da7a5e0..960aab00 100644
--- a/offline_tests/ticket3i_3_e8_1703.lus
+++ b/offline_tests/ticket3i_3_e8_1703.lus
@@ -70,7 +70,7 @@ tel
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
init_a1, init_a2, init_a3, init_t : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var p1, p2, p3, t, s, a1, a2, a3 : int;
erreur_ticket3i : bool;
env : bool;
diff --git a/offline_tests/ticket3i_3_e8_1703_e8_2560.lus b/offline_tests/ticket3i_3_e8_1703_e8_2560.lus
index 168f4198..02e8c1d2 100644
--- a/offline_tests/ticket3i_3_e8_1703_e8_2560.lus
+++ b/offline_tests/ticket3i_3_e8_1703_e8_2560.lus
@@ -70,7 +70,7 @@ tel
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
init_a1, init_a2, init_a3, init_t : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var p1, p2, p3, t, s, a1, a2, a3 : int;
erreur_ticket3i : bool;
env : bool;
diff --git a/offline_tests/ticket3i_3_e8_1788.lus b/offline_tests/ticket3i_3_e8_1788.lus
index 5da7a5e0..960aab00 100644
--- a/offline_tests/ticket3i_3_e8_1788.lus
+++ b/offline_tests/ticket3i_3_e8_1788.lus
@@ -70,7 +70,7 @@ tel
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
init_a1, init_a2, init_a3, init_t : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var p1, p2, p3, t, s, a1, a2, a3 : int;
erreur_ticket3i : bool;
env : bool;
diff --git a/offline_tests/ticket3i_4.lus b/offline_tests/ticket3i_4.lus
index 6a64f8c0..228d75d0 100644
--- a/offline_tests/ticket3i_4.lus
+++ b/offline_tests/ticket3i_4.lus
@@ -84,7 +84,7 @@ tel
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
init_a1, init_a2, init_a3, init_t : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var p1, p2, p3, t, s, a1, a2, a3 : int;
erreur_ticket3i : bool;
env : bool;
diff --git a/offline_tests/ticket3i_5.lus b/offline_tests/ticket3i_5.lus
index 8186719b..16345d9f 100644
--- a/offline_tests/ticket3i_5.lus
+++ b/offline_tests/ticket3i_5.lus
@@ -84,7 +84,7 @@ tel
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
init_a1, init_a2, init_a3, init_t : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var p1, p2, p3, t, s, a1, a2, a3 : int;
erreur_ticket3i : bool;
env : bool;
diff --git a/offline_tests/ticket3i_6.lus b/offline_tests/ticket3i_6.lus
index 5c186239..cbd691bf 100644
--- a/offline_tests/ticket3i_6.lus
+++ b/offline_tests/ticket3i_6.lus
@@ -84,7 +84,7 @@ tel
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
init_a1, init_a2, init_a3, init_t : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var p1, p2, p3, t, s, a1, a2, a3 : int;
erreur_ticket3i : bool;
env : bool;
diff --git a/offline_tests/ticket3i_7_e1_2192_e1_1852.lus b/offline_tests/ticket3i_7_e1_2192_e1_1852.lus
index b772b0c9..be141b26 100644
--- a/offline_tests/ticket3i_7_e1_2192_e1_1852.lus
+++ b/offline_tests/ticket3i_7_e1_2192_e1_1852.lus
@@ -70,7 +70,7 @@ tel
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
init_a1, init_a2, init_a3, init_t : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 4-induction;
var p1, p2, p3, t, s, a1, a2, a3 : int;
erreur_ticket3i : bool;
env : bool;
diff --git a/offline_tests/ticket3i_all.lus b/offline_tests/ticket3i_all.lus
index 9acc3334..bf2b31cf 100644
--- a/offline_tests/ticket3i_all.lus
+++ b/offline_tests/ticket3i_all.lus
@@ -84,7 +84,7 @@ tel
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
init_a1, init_a2, init_a3, init_t : int )
returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var p1, p2, p3, t, s, a1, a2, a3 : int;
erreur_ticket3i : bool;
env : bool;
diff --git a/offline_tests/traffic.lus b/offline_tests/traffic.lus
index 0d0bf54c..61a15f0c 100644
--- a/offline_tests/traffic.lus
+++ b/offline_tests/traffic.lus
@@ -21,7 +21,7 @@ let
tel
node top( Delta : int ) returns ( OK : bool );
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var Total : int;
let
Total = Store( Delta );
diff --git a/offline_tests/tramway.lus b/offline_tests/tramway.lus
index 165e3b25..3d47ca04 100644
--- a/offline_tests/tramway.lus
+++ b/offline_tests/tramway.lus
@@ -142,7 +142,7 @@ tel
-- [explain] +------------+
node top(request_door, warning_start, in_station, door_is_open: bool)
returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 7-induction;
var
env_always_ok, prop_ok: bool;
open_door, close_door, door_ok: bool;
diff --git a/offline_tests/tramway_e7_1834.lus b/offline_tests/tramway_e7_1834.lus
index 44d0784d..6680b30f 100644
--- a/offline_tests/tramway_e7_1834.lus
+++ b/offline_tests/tramway_e7_1834.lus
@@ -78,7 +78,7 @@ let
tel
node top(request_door, warning_start, in_station, door_is_open: bool)
returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
env_always_ok, prop_ok: bool;
open_door, close_door, door_ok: bool;
diff --git a/offline_tests/tramway_e7_1834_e7_2363.lus b/offline_tests/tramway_e7_1834_e7_2363.lus
index fbda9403..80982aa0 100644
--- a/offline_tests/tramway_e7_1834_e7_2363.lus
+++ b/offline_tests/tramway_e7_1834_e7_2363.lus
@@ -78,7 +78,7 @@ let
tel
node top(request_door, warning_start, in_station, door_is_open: bool)
returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
env_always_ok, prop_ok: bool;
open_door, close_door, door_ok: bool;
diff --git a/offline_tests/tramway_e7_1834_e8_3192.lus b/offline_tests/tramway_e7_1834_e8_3192.lus
index 5c915be4..74f0a68a 100644
--- a/offline_tests/tramway_e7_1834_e8_3192.lus
+++ b/offline_tests/tramway_e7_1834_e8_3192.lus
@@ -78,7 +78,7 @@ let
tel
node top(request_door, warning_start, in_station, door_is_open: bool)
returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 7-induction;
var
env_always_ok, prop_ok: bool;
open_door, close_door, door_ok: bool;
diff --git a/offline_tests/tramway_e7_3304.lus b/offline_tests/tramway_e7_3304.lus
index 44d0784d..6680b30f 100644
--- a/offline_tests/tramway_e7_3304.lus
+++ b/offline_tests/tramway_e7_3304.lus
@@ -78,7 +78,7 @@ let
tel
node top(request_door, warning_start, in_station, door_is_open: bool)
returns (OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
env_always_ok, prop_ok: bool;
open_door, close_door, door_ok: bool;
diff --git a/offline_tests/two_counters.lus b/offline_tests/two_counters.lus
index 60e10745..1886c4a5 100644
--- a/offline_tests/two_counters.lus
+++ b/offline_tests/two_counters.lus
@@ -18,7 +18,7 @@ tel
node top (x:bool) returns (OK:bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 5-induction;
var b,d:bool;
let
b = greycounter(x);
diff --git a/offline_tests/ums.lus b/offline_tests/ums.lus
index 1e4c64da..560729b7 100644
--- a/offline_tests/ums.lus
+++ b/offline_tests/ums.lus
@@ -55,7 +55,7 @@ tel
node top(on_A, on_B, on_C, ack_AB, ack_BC: bool)
returns(OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 2-induction;
var
grant_access, grant_exit: bool;
do_AB, do_BC: bool;
diff --git a/offline_tests/ums_e8_1032.lus b/offline_tests/ums_e8_1032.lus
index 3e1035f4..a03d25c6 100644
--- a/offline_tests/ums_e8_1032.lus
+++ b/offline_tests/ums_e8_1032.lus
@@ -43,7 +43,7 @@ let
tel
node top(on_A, on_B, on_C, ack_AB, ack_BC: bool)
returns(OK: bool);
---@ contract guarantee OK;
+--@ contract guarantee OK by 4-induction;
var
grant_access, grant_exit: bool;
do_AB, do_BC: bool;
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 5b55f474..73699153 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -500,7 +500,7 @@ module PrintSpec = struct
| _ ->
false
- let has_memory m = function Val v -> has_memory_val m v | _ -> false
+ let has_memory_expr m = function Val v -> has_memory_val m v | _ -> false
let pp_spec mode m fmt f =
let rec pp_spec mode fmt f =
@@ -512,7 +512,7 @@ module PrintSpec = struct
let mem_reset = mk_mem_reset m in
match mode with
| MemoryPackMode ->
- self, self, true, mem, mem, false
+ self, mem, true, mem, mem, false
| TransitionMode ->
mem_in, mem_in, false, mem_out, mem_out, false
| TransitionFootprintMode ->
@@ -525,7 +525,7 @@ module PrintSpec = struct
let mem = "(*" ^ mem ^ ")" in
self, mem_reset, false, mem, mem, false
in
- let pp_expr fmt e = pp_expr m mem_out fmt e in
+ let pp_expr fmt e = pp_expr m mem_in' fmt e in
let pp_spec' = pp_spec mode in
match f with
| True ->
@@ -545,7 +545,7 @@ module PrintSpec = struct
fmt
(Spec_common.type_of_value a, val_of_expr a, val_of_expr b)
in
- if has_memory m b then
+ if has_memory_expr m b then
let inst = find_arrow Location.dummy m in
pp_print_option
~none:pp_eq
@@ -582,7 +582,19 @@ module PrintSpec = struct
| Forall (xs, a) ->
pp_forall (pp_locals m) pp_spec' fmt (xs, a)
| Ternary (e, a, b) ->
- pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)
+ let pp_ite fmt () = pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b) in
+ if has_memory_expr m e then
+ let inst = find_arrow Location.dummy m in
+ pp_print_option
+ ~none:pp_ite
+ (fun fmt inst ->
+ pp_paren
+ (pp_implies (pp_not (pp_initialization pp_access')) pp_ite)
+ fmt
+ ((Arrow.arrow_id, (mem_in, inst)), ()))
+ fmt
+ inst
+ else pp_ite fmt ()
| Predicate p ->
pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
| StateVarPack ResetFlag ->
--
GitLab