diff --git a/offline_tests/DRAGON_1.lus b/offline_tests/DRAGON_1.lus
index 42ebe80b67dfd61ee4cfd2e3d77450cb8e981aea..9eca443b41914c3e4bbb909d2ea13647d840dc2b 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 89106475ee5e55f207792e88beecc1e66de5b29e..3a5d625c34c4052a782ff74c5afd91cf3bf73838 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 2b4710aecb884f872aca48f4e87957932dd55629..98e5642022f7c78d38d7914ae396a093846a8bbc 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 cedd86b2ed8bde52a75d34b16f8ecaa507f88109..4f656dd102a009413f5c64d68a887d2c1d90d871 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 448bdf459d62408d21a222f4d96cb5c226cd8a2b..ea84210b521c04d1fc513346dd074bd4253fab95 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 5d4db2242881941a03e85470df38e25a5b16c06a..b93e428d94f96b989e315b317c4620acd0b5aa7c 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 31cec0364a7690c16f09ed6a2eab352e99b7376b..f423cfcb2727423859a676a4970fafdac52ee34e 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 f53af9fc176ce11e667ae5bee98327d94cac8566..5f48ee4371bc33c59092a4cb9c797c9050fc5a3c 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 466636e13fb02a4a204f657b46e3272f73911894..7670834c54882d9ff0e96f073344e63ad97b4042 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 d91e6cf1f49bc359f62843ce7f0d6f3180df735f..175b69ed713f099209af2dcf3917ae76d9d72c8c 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 56f22c53ed38aa9ddb9dcfeca0e84c51cb61bb0a..dbf20fbdc1c175a071a7ad14a075a1ff7b59a737 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 0216eb2b880a69146b11c73af4648444b7288423..511cea81a9d922990bb84d167ccc996a45d4d82d 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 1d523cf57a656544d3e311ba39c2d45fa3b1c93f..3d5402e19ff05ae345e64e332f69332cf8447ba2 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 f8e39ae5673cc47ec2831c44fc0acb0b7409fee8..7c3c611bce687adc8c5dc82a7c3c85efc4ebf68c 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 b872109f0adf7bfabe508245abde847c0d1379c7..b124e5aa7b036e04d9f9c1d302943c35ebf30fb2 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 1909322bddf4f22aa675b6fb2d0b4bf7c44f2778..7d1042e7db77e20c204d43d69ef6cfe40fed19ce 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 f8bdbedee1b08c4ab1088dbc29c8de09840dac58..f59ceb1bead89360430e45de88f4f928be7c8831 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 5927c29af5010b6ff71e26e762ed35b7bf9f0649..05973d13d3c926ca234f1ad14107f9aac9dc4195 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 b1db6758dd07ccf9abb1526eaff20cdec5471c57..f5358d9dfa0a993eaba5be332c85bd7b35856462 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 7a666ccf0218a77ce96df3bc528aa527bb495170..4c23b900250ff15515997406f489c58fc8fb5c6c 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 b636f732995bef932b9b9a8a7d5e23d03aaac5f2..a5314027d829130782fdeea303b4756ae1e7afdd 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 9827b465611e3e96a797ce070efb10eaf8a45780..029f44228667a9fc2ab9eac3a50785ca758309b9 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 ddea8c1234cea98c5fa6da799aaabcd8b8ed039f..2dd1c5e67e47977c8af46a5042c8bc33a443c3db 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 c265ee177c5e1ac65448fb97053a0ec5a539e09f..c24841a6a2ec4e95745fd30796039b23b095a55f 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 226e2e76c899576e0e107c050b39f910ed0f24cc..10fd88252c579b9fb9c7b60de5cefcb61ca72825 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 e7cee1bb4003c39f9ea5c99a663f08e6bdecd871..5e9428a0ce556ef947dd143bbd74dfe41fedae10 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 2cd5978ad43c273c0229bb709c3223fce214a51d..ff8e404b85095899e32989b40a77d7bb2ddfc617 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 f5aba556826ecf88a7a2c5452e9a7734e12c113a..dcdd3f5e82c4de6551afca8d7a088ce9820b56e4 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 072b3d2819b9d83704b8507d1ddf8d5fc27d5990..44a208543053a835e93e6a4cec32c480e533f8bd 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 1bac970b995449a07cb0e3b730af416375651ba6..27c4fa98c45a4c84860de06f5b8f966e80059c54 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 f0d31ea6f811b88c71df190f212b0e64f46e66ca..36ff872dc87ac7d3da3fdc37efc8d6370b102a46 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 c4957848290ae306db0430e2ba95f0a9092cc448..eace68f4b9593027b0a28ea88c5de826058feb71 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 edcecd3f952632010f514d955f56fe7a80cbe04d..9f75bcd8a4a1f535ad107453f5fa89dca0138721 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 479176aab6f2317423d90ab9638fb2ec8f58af9f..5025b27f38e378c8fba6fb67d2e33421eea53b95 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 88451ee5ebf9d31d7551c5c6c894607cc8fa5dc1..bd89765c591c2db27cd746ef55be6e1cb635660a 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 5cdd1ab09bf1b146a3acb582e568320358be3a96..cba703d5377410a009c0c01c8678c4d9a307e085 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 1af9e87a0fa28542f8ff7b345b475dbed8fda065..09fb573ca5a2db3fe0afd313eaf5f5d0aa89c806 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 862513c44616029431dc3867546f65a2914c57fe..732c6608acf9da63bd2c679e38ec7571b727d37b 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 913649f91bc34aa6584a9f9fdfdca0a6373914d0..b1583ee08058e6a106be5ef0fde1d5a17206fae0 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 e382d85ced4cb5b440086a7d0c0a06f73e0a7fb9..d9203e6d5d430b94f50ba5f091b6d0a0504648a1 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 20f787e0fe4646817595816adcdac4a2f19c33e7..dddaf0fb3753aea58f414f1f9ad276a0680e12a6 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 9d77bbf324f42b3f1fe54579998a8e1cb438e9da..835e586501acfa3c2f2d633df24b09c570731e62 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 abe55e7b00b15a313a602176428ddbc28323052c..9dcd1c0ca1100b63228cd0109264a4548729b60f 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 8b7230dbcce7df32294e6dfa71ed519ba04c9211..4dc048d3476cc41b370087e86c7a78805eccba9b 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 7eac2360e0a14f2b4742713bae0d43a40087deb7..08f4bbebae7d428c1ecaa23f0e1e40e5294b70a1 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 bd939ced8bc96405ef8442bbb96ccd2d107218fd..1b1d6588d705bbe911ec4d4b7a0f97d0e1ca6ffd 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 18cb3c1bcb51345d1b3741982b29dfc60c9baa53..32b524d8010710b375a2f8becaa572008f3f37f0 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 ed84e7ec1c5bf086062e974eb2fcb33f3215607c..54f6228a82f03218d21af47f1bebad34cf4126ab 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 3b446311356d2a96118ce32393d4b9c3dd6f5363..bfa923eb695754db4fc56764f2c652e3cf7d5282 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 7656b5fa98dcdd5f2bcb7b45036cbc7255ea6d53..6f4d84e61bce34eaf3ef5693854100f1c7928b82 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 49b3f491bbaf06495cac257ba560dbb66d2a7fb1..54cf49a21aadcd4b18e5c420536045bd23dc4ccf 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 e4863bc596da04e9c8edcda1d3335bb8ddfb040f..3dae3b0e5e4dc6cb199d2639fb00ff162092169a 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 f1f97e228ae7d72a2a8b2da22d0bca27c2667fc9..58c31761ea4ef26ce5925f98e0ceae242f7ed54a 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 5a67c87d941b3193589bbb531c9b72db9c98eb94..b60e4ba5244b8ebc41949ef373e4897a73faa843 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 15f23c71bdb04222e823a7ed6941e1e771684110..e854b885e3053b9acba26078e9afb56d345c4c2e 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 cfe8ae48a4d8bb50ce9272de5137d483aa985f30..9a307a7faaad9b4743251e8b4e840b5c40806c29 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 cfe8ae48a4d8bb50ce9272de5137d483aa985f30..9a307a7faaad9b4743251e8b4e840b5c40806c29 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 174277ceeda4c0ff04aa84dd109fee702775b35d..2f1de3c5f375eafb9c8c43e5479a9a06fae429fa 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 1187d84586f459a6601fe6a1141ada74c9c6eb29..d6a63e765d90cc94d50a346e1e8290e203cd7a57 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 f5c18b70f19444b470e08fc9e4cb815a86719be8..259ce112b889476a4d98b89c0e6a75f450b1da0a 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 bfe828dceabdcc343907056753575ad8c0056451..1bf612aece5d5025dcf8dae6d87ba75ee9c30d09 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 83d24ef7eea05620fb8f1afaafc7068094f21950..e40fe58e3ca129e273828bfd0b67f251e672e302 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 4e14db8c03c7752f8746a703ed5576121d282400..cbd852e3d27393782ded4497b89684d8df368935 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 43be305401013ebd373739699c655f39d9fe4db3..da4f57a9eb38cab241d6b4d60e675a8dbc82e3e3 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 0d8759d4115404684fe6d060566d46a76e4f2ee4..d5a6332a2bb5fc47bcc2de63e4aad79d1082d4ec 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 922b470aad115b15fb62f547f1241111dcc827ff..2c70da555f5cbd3ff5b55723aa95f796781c81cc 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 075bbd7631f362436b2d5d532e2d630bd1d21e91..b2989e341e69ba4733bea6352b44086e1184517d 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 19261f2825b361b1d2515ba48855bbb9b6c5e37b..885bd8bb6760c47ee47ac249806820e3a24243fc 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 906f371b4d7d721bcc86f8a87e7738ba06b5b849..4713f8f763256f9ba80e0b168c711517798a5089 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 46927adef8e25da5347388c1754e11fbd9593fc3..215db0a06b9cc7c45942beb870f9317889bd31d6 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 863abe15da9ff0909731d25c74788b1722c4df11..22ea78515ac5d5cc04c13349aa1f870900d7fcfd 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 adb9d84c27dd292f18de57ecd69d6dcccb54ed5b..264163f194c6970488864af5efd962d8353f26f0 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 10608fc83b8ce5f0882e258a4786c5e514889e30..18d65e94f2fa020f858cc90303fb3ecc3a298c2d 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 4422064dfd7a2578a9658916959fedaa5dc523ac..6f1cc5accc77f046e1ba5ab242752983738349f9 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 e280dd7d484ba581ce0ebc058c669ccdc56478d9..74bab4f84fcf3edd2613aac58fb808d9b10e3043 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 1d947a549f68c4973f2caadfd6434a945585d794..24057f2a853e4d206bab099aae2f32554f65e64b 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 d8425493540b9705ee73cfff6f0f02947c7ef5ec..b8038eb9295f7df6b5c8acc7d0f01938275b7253 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 71fc0a5da17641f15d83d02cdca77bbdf4805943..4b4f0f6e47d464fce3d37bbeaf672860ed08b56e 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 aef254d6eeeba04dfea89f1e534a8bebda50a509..a16e823b04329cdebc2ef3a131e0003de3cc8d9a 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 484221be00ae0f27dffb389c721fe98828489f46..999649530b8d1aa8f4380aaeb42efd6fb44f0105 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 bb2bf3bafdcc1d30fed32401d3daaa0052633cc2..030326edb4c2643c427133643cb53ceec18bc159 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 bb2bf3bafdcc1d30fed32401d3daaa0052633cc2..030326edb4c2643c427133643cb53ceec18bc159 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 1476497cb917d85542a1ce0234b55c438b1abe9c..147cdda7b3771db72c7a1778a3ddc3cab2bc8a68 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 17b18451c3774a0d2abe747988701d74a9360f2d..f5aa1a15dd6bb57ff820d1aa2adf3aff185b2426 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 c56c6f8f86572d0f1de48eda4ca3e77c951b9b9c..5fb7577c1acf16dabb45a2487f25564936b4f84c 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 4b40938e69b68371a6f0b59a6eaac30d30e4cac0..fccf963a615a7079ef0de2dbaa4157dde7a1bb07 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 b5fcabf0fbc7cf396ef3eaa8897b11dfabd31c0c..40ecc2da3ea0fffc3d9ecd041e021bbde1fa86a6 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 6549ace01bee17dd1811d52016075b12b0fdd8f4..09e5a4cdb317aab5fd18f53529991c974b91f33e 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 0643e78672d2dce7e0fcefe70628addd3f752436..bb940dcf542ada958c27396547213feb8793e2b1 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 28d58e7b2b29c2c5862697560527935f6fc4943e..e689df9e53f7cddfe1003b746eb94db05d25f57d 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 5e82c228de4fc7c7359fb2070c5e6636d380a6cb..31ccc974cd89f1c305dcafad03189200bd3c757e 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 923e84e4da1212cda0fcc1a3cf86b929b06f2b79..d82d5ed82f72254ad032ba4ba9d0fa54efbc7048 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 6d4bc58e32960eb11848376ef7b59a614306ff00..c2a893b1d02cf51e3a73f7317ad4fe284a23a3da 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 d43afddb9f732fc7f2304afc8b8158f004596261..cc85a37af689940ccfa291da5d8a040a3ea8c606 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 fe1f91f78de666f0a82a8285a2745deb4d7c9a07..bfb903a8e80ce212ad2d4ce058074149bd1a9601 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 631718f62e49b2391998991915751f92463d10f4..f6405f4155b33584d929531f36802d629db16bb3 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 ce6a14daddfc3bafc9fad5461f5ec4f16fa44bda..43df9739c25702d3c4d3b1c17e3f5d8d94f72cb0 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 394323de01f344fcb2630ed5500ad9d1a4c21053..95852e6c10e98923fa70801b242c33a9cf8d733c 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 635c8783349292fcae0ae5f281e7afb1b551f69a..f767daa621f4aeb1d6ae4e8b98da95bfebe19ecd 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 468cc09ce38fb32f315969740a6fd296e54c8cbe..678f84c08c668530aa2d49aa6099000deb61af18 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 937a7da53b6bdf8d9c59679d8840d74750921cf6..618413d262361624b60734ab3ccdeab05c5708bb 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 f42ecc65f9e15b22b10f96c302058c28da24ecd2..80bf9ea54ae040bc13c3638ded52edda9fca8ae4 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 c05de50919caa0effce5f987f10d8c8960c36dd5..0c2561cd3366517a93e473f933a8fa910f0ed28a 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 c1a567a1d91703f5d3811d2c05d4ee16c0427ef4..7e5da70462e0acafedc9197922f2f128fec0145f 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 e6c252c50f4182f36fc6bf5557dccbad9fa263bf..614fb5264273f8678f62f6bcc6c911c93ecbc121 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 3533482a4f505b60213a9a207fc40c1df2cf28ee..b2490695f8a06de0d7ded4d364cbc31c275eeffa 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 e44090ab1f7e0cc5d5cf447e3a6b7f1296b234b1..c1ab3d7ff84ec8e44f25b9ee9f483076a310d71c 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 e44090ab1f7e0cc5d5cf447e3a6b7f1296b234b1..c1ab3d7ff84ec8e44f25b9ee9f483076a310d71c 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 568cdc47db7cfa057d824f853af65cf110ca21a3..da8237d6b0b6cc125f72a14c2c69f3c3257c3b98 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 a76d0801becf5eb720424d1dcd88e4077bac334d..3d89e0132abe8ce8c72498502ce6976448df4b81 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 a76d0801becf5eb720424d1dcd88e4077bac334d..3d89e0132abe8ce8c72498502ce6976448df4b81 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 e186f9466ac9c685d4de143f9d0b5b27fca61d7a..5dd3f7929071bbe64967a98a014a71cc4f5f1cf8 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 ca32ed1a83de1c0308d1a6375973fc29acbd2796..ede5e0f4f2078a5061e0c16d2ae3c54b522a9c42 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 c6555bfc26ce7dd72add34cbd1e93de978a3893c..c596df4648834d1374ae09d9aab1d2a744b9d753 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 fb1e20553216e407375c25fa1c7698a486204b8f..5c4635ff6dd2f0173ccaca2d84e2f3c942e99f86 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 c6555bfc26ce7dd72add34cbd1e93de978a3893c..c596df4648834d1374ae09d9aab1d2a744b9d753 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 8d20b92d1155ce05136e1caa48216b280c2c9045..f6895a969ae11de1b60d9e42e533ee3a87a0d433 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 8d20b92d1155ce05136e1caa48216b280c2c9045..f6895a969ae11de1b60d9e42e533ee3a87a0d433 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 d3125beb315d1f55d54fa4273ed900bc4fd4ede2..e156c0502b71157ec1466130efbfc4d11e06637e 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 568cdc47db7cfa057d824f853af65cf110ca21a3..da8237d6b0b6cc125f72a14c2c69f3c3257c3b98 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 fb1e20553216e407375c25fa1c7698a486204b8f..5c4635ff6dd2f0173ccaca2d84e2f3c942e99f86 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 4781b350b965df31bb6aa7e13e2da678e5a2b3ab..8a7df27c70f0e1d625f843e3fb1f5ae8422fd443 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 e1d260492197fd5b9f44b9044592714fc8ccfd15..ae1abaaf8ac0a8602c6e6448a3dfecc6d9a1f708 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 3e6d2102da9e0e8dd9dbe962f7adb064c3b3c0a6..a38ec0a3d1fe6bfe1b0e04b4bb1ff285baea291d 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 f72972976482a38946ca219238e635b6ee56af69..1adf15aa1b062ef36a3a09b466f6cc555645fbf1 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 5ee072ad183737e0b0a079e0a0b3fdff6c802964..c619b794c925364f0ece14b9b7c906a6362c6335 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 d05526e76ed6520081f5df9def5cde3bbc83a607..27a901a5eb1df6076b9befe770ecadd0b49a2743 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 fc673e0bbf7704b6c7d1ee162b39f0bdd32316d4..7bc737ff443c00d7546e3ae04ad2d9b2065995ce 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 9de6067c69725f7fb5864fbf05c5c32915cd146d..24357e4222c58606358af40d3aa03b73ae647ba6 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 4bbf3ed2bd0b25f137cd1544789b9252915e3e28..e0b9084dc4e715155c1a67d3a827d519bcad6484 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 89d0be60d8b720b1f1f048a836195651d8f1d44c..0db434dbb38eb4946571f9b8c4bc13fd510b06c0 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 6cb24a14a818e9f123162b82c7b089127ba575e3..21af8a4520674803b443a163bd73e8825700d04f 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 84ae2878f4ed4bedccc4096da85250c6fd32bd83..c72d0d7a36e41c1d4aec99507b325b0865d34b4e 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 76add05a843f6633823a5f63d3e3603d4d8db568..c1b97ec22b46d9e90acde0cde5ee2fca92d7f0bf 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 cdb22969a21f218af643bd1695c39d45eba83f10..2fc1a0f17aa592223b42dbe7dd93e5e8d4aa3859 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 51559f0738a85d12fc80d5a92bb4083f390aa458..3300c2d31319d8386bb56212118d06b8df0625cc 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 7d8173eb73d50e24d3beea4a01053b075537f642..fb7b0a9e229b3ef5a15062faa9240d3d3cccbe90 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 c1a948a62cd569e1a281a4d911ca4a22360248f9..b717c8b40b16c35c441ee1344b59f11b6859da49 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 446522c79b30c5efbf4b04c11b5aab52a76a7f3e..26937607645db6b45a3ae8d32cb55b52eed08d66 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 ff4242eaee4cfafc40733be7cd8aa6386aad713c..5bd990249734ac6dd5ffb9e110ce9f60a2300931 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 0c4ac350cd4e45a192c78ea5727b452405d356ab..b77bed281676aeb4efe168d16262acf637060fe0 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 b4ab9e446f2a33bc7dc80e2638249ed8378a2475..e589b510785954c2f4c685249ed5a098e6c7fad3 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 5cedce95ddedc50cc4fa1389c9e92d43e325af48..242cd743ffa71b45220223bf611b6df041db2528 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 04e45355df6cb05d000af4651c9ed72a0e24d69d..401f4b4ee79f16814ce1d648a432009063c3b575 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 a66d91cc21a44a362b32421dfd756794dec0c8dd..e2bde05b7c082e73c0010d0573ac88de77776d8f 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 4a91ae6bed3c80cdc335afe73be89f9575e9b045..7724d5120011c4329fd2a5001854ba802f78b894 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 cc9667b2fbfb0036a6989ae9d2c09cdb952f069a..29cff96d1488b85676a88f518a3db865bd9577be 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 73d2a280705a6698f0f32afc8932c5cff2d3be0b..c2db03c22dd5bff2e1ec15626a7faddd818cda15 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 76670ccc0b53c12fbbb837b1d9fdaa9dcf9f2a26..b06a55f587bfd73fd6360e6aecec14959347b813 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 76670ccc0b53c12fbbb837b1d9fdaa9dcf9f2a26..b06a55f587bfd73fd6360e6aecec14959347b813 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 21500249c2618715dd0abd01afae445076cc2d6c..c7da573c1ea0d7ddb85a2da11c54fdc88060de44 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 56781633178182375d5356b5d26e573a3915b92c..88720c0ea738ecea80e4c773d8c637b335164634 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 1fb0896911d2e6f4d91b44a8aa6258931ed62a59..a9a4d34c0db4ec8175f003982713f911de95d5ef 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 8c28326bd9f7de225a8c35dd057cc42cb58ba345..ad0186dec4b4c9af3a4206a6ec5c6efda5bf51a4 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 6a085bfd543a91d48110d4957126784971a0dffd..6057cd46d4f98a1e55269362be76b945caf1f9c7 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 f0f7b4e1705c8c823eff45186866c916a8160b60..97990edec339dc3c384e82638181268b0e6f4986 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 3a7dadc6b0cd18cda681d4a78e82af095280c1ea..60809ce970cf7f032b582d36db949537f1a0675a 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 f9f0bc1e0896e982d663cdb0ce9ade04c8c2024f..8322086f029a4d30bca552d75281b2d5f0aa169e 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 63450434421505840f6e0b2824bb540db8b1cbd8..9ee8188762093334b84799a58c048fbc818844a9 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 fdc9a994f394055b84b8195e2d505e3e7f47715b..b1be79aa10d470e8f0e0f5647dbffc0020396fa4 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 793b45111724969be3abb2119d77247a628e9c03..a4fe26d4039f48a61406e7dfca508c745ef6fb1a 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 817b90f3f8b9c4baa75b4080d70d02f56a2e5377..228d9bb0592d0b3d61cae4bcc9deab7cf7ed2ff3 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 9b9984bd86719007c74f2cd580fece5463ad8c93..0d08f572abc5958003b031b3151a8f7fe5bf274f 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 748bb8446095fcfe3f6564e8ba947da0b2833414..418f81c0a359f69500ea1989874fcbace3ba7e7f 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 4c4780b790188ec2c6667901973848b380749767..203645ad954046b43d511700ab1ab8a5b3f73afe 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 c09270de0c275be7a442c9f95083e87af6bc3462..74887a35d8ea9c855d2e803f0e3c30ee1ec04d1e 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 67af0df13fec18cafe5121dd86280ac274829abd..c010cb42b69f67a5adeb50910026eba4760cbc16 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 b9e523fe91f543ebebd9176e2224f6d0fa7777fa..83a3eccb96ffb9968f499cdca9920cd392ee777b 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 64752e0a896b67f76f21dc851cae70c21d1211a6..a11e24510edbd1c18128e696d30b5a2026cdba93 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 6b76d4b7d9c7e5c6bc297532bca50fe430804431..c22dea3cf2708dee1c3eb28635d51e0d5c79f272 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 d34ca65cbfde0de6d40e894d2512dc3c93a7bf81..93e240eb57e5e6ca3a4436175a7dbb918821210c 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 1816a1bf9c6366ce8d71991162ddc4c8409c8c30..ef1dadd997f3b4aff084969588097fa18843ef2d 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 49dc938a8a81286c49dba9e2b679352e9b67a072..f46f87e3b8b10f4ce0d7e5a715f99bcaa33be6a6 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 593c5a106ae34caaef833f2ede52d0f64359b4f1..bf480be0c42764d246ebe5ec77e074b22f6a82eb 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 d8a6aaa3dc9399d1cb1b6602cdc7ed5324ab5c5a..ec4e03d03b1b56f8bf66b8af7b271319a9b0f395 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 722ef6a9356b5fd3f266073fae821647e5b25abe..50fbd31412babf23d00e90b88e0feb7372b46843 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 bb73b0a7d487aa4bee5fae36abb20988d52183cf..d7487fdf9bd699f55d56507fad1d8a808b8b04f7 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 db58987b13a7ef0639b27dcf545ad53b5fe10b04..f0d02c50fc08fced12cf8c7a082268498a20222e 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 c0a9c73dc288bd28d2dfd7e95117b3cd5da25911..e4b00e9f7019a7d446a1e9b4d349cd12635589fe 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 b80f933b1e6db953ded824b1f6ac2f8357092113..0cbe8e636c4f8dcc73bda17de6e11bfbf501061b 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 3720463d5850fdd8ad01a7377ac5871aff69a8e4..f211180fe022a0fc4d7d49f7e8bb69041f547046 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 433fe208386b0710e2eb18ca9ceb1ab625401c19..4af5824716656e5b46747065e1db3800cc662091 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 7730678e6d9b7e65e3b47628b89ba006a2931f8d..521d44e8c58aea8df6034e0ea49bd1250d440e7b 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 92cb8ed7e81893aa416c7b720b3fa011bdd68539..b9cfbf5d0706eac85f4ebe6781d45c33f203e85b 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 b8c0be1ebbbde85773eb9aa5191cacea8e53faa4..a688b0b1cd6d4c6288cbea954d71b0c52dfd0248 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 6870dfe4c12f55b9ba0c88638646f8d5fc593e07..45bae14c10744fcd97ab7b109e0470344ad42ce1 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 7c9ae780ac96891319c9c14a3886e841a74c4ebc..d0e84ee4ddbb0be5af6d96b6da9a93905e5e2a1f 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 29596418d74c5f9c2fdea73d507720709578ae14..3af57bdbd3f56747dac66579930fc81142cf1024 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 11fcf68c41578117528e21d6998a621ca363512a..44d06ff2257350fac8be6aaaa36bf0e17e3464a4 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 5bd482a0c93434fa0df3cb0dd56676c516ab6a1e..bf9a367f802d893db698210a1eb8ac6730a7f1b1 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 d9e7cded65b2db4c1986e4d9add832cf0cef6cf1..a5c0dd8476e6d21a8e938bdf15240b9ab1f28da6 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 5243cc181183cf22b6e35251a58b57cbf8eca028..6a28c7c63ee3682a5f962eb0b070050bc6ecc0ae 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 5243cc181183cf22b6e35251a58b57cbf8eca028..6a28c7c63ee3682a5f962eb0b070050bc6ecc0ae 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 37773db04828c03c1674222fe63cf2ecb2cf7df5..0e4f6c2da614eeedf20bfde102674259932a12ef 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 37773db04828c03c1674222fe63cf2ecb2cf7df5..0e4f6c2da614eeedf20bfde102674259932a12ef 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 39f63ca04271d0b631ed64331b0fb4bd131386c6..a416e58f0c19d18ea61562f9f1673e0385599bb2 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 649de53e4b09c04422cb31a1576e85e6fa0c16cd..6ef577a60a75e809c58d9b128e44af47f597db61 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 fb3000b6b26ab657c162bcb4ac1b3087d2e24404..5bf36dd2f1d1c69f86d4bced4e8a7c314310cd09 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 ac5941b34eaeb320fa3a05fb4297cab9fcae098d..0c8868d4ab1df1e682bd05e3304cff889d7747e1 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 9320f6c7777aa75826ae2ffa7264ce33f8317ca3..e7e1dffb86532c01f9ef01bb1a120817e93d40d3 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 397a66a1036bbab9ea000fcd5adefdd3cce1800d..693fc6aebe4bbf5ebbd3699a90753a6f692f2e3d 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 709872be72f1d282a2bf6de244b9529be5d19604..ed76cdb1bcfe25b1d2244ada0254f079c4ecca57 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 90ec6cb42192d58b0972c9202663d1d9bf11a299..db939b2f28dcdaffed63797fc90965d1e2674e89 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 0cc5333ac883f7b4896d578c6cfc770b2d6b5f18..adf76040338e5f236f152f9d25f18366f770ad49 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 6a52b5acf1ae27335a72af5d9ceac8cf82b5eba0..c30788301817cb2f8fa375ec3423f6dfba844e56 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 7f6342e716419e93880f1807732c13265ade289f..36ed799d0e7b040148c1a27bdde4ef711c7783b8 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 2c1dd082a1fecd5a51b51ce9c11c56d79e2bb0b8..e13821c15704c2da6f59485588fd32e391a0d5fb 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 112226e4e2ecdc47195b41f6a7907ce78d473d93..3cee21b4b5e019675c6aa409a1e947f06660ad9b 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 a75e8768f2e26c9a224c739b5b8f07994e68ecef..4a82683ae31fe8a7f644031034d6527f6f0697a5 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 4f09bceb1996142c77daebac638a8200c3c06ff2..5e75eacc7c77db2c51cca7a6bf5aa5674361f9ab 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 a83d56cbac82e355e6202da7b276063d7b0b2a37..c741b3ea36c65a435cea81dd3a68442af752fc51 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 fce911b645a24ec7f3465a6b62e3c9d6974f9635..c3c93cde17cfbae07d846443cf49539be586378f 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 3b6e8acc8633dbee0d8ea9647ac01fcf0deb61ca..8c98a6412b34a3c7342bce62aef06baf9043ec32 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 70df17dc869f823c557eb229981a66f41edaf650..83b0f86eebcc02bb4edcd4d033e8b215500dfa46 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 df60671380ef2fad9b220e9e40ea0a0a4ea843a0..9718c5a51d234f50c75e31889c9092ed73f7605d 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 80d577e5ab7b89c11600aab6537a80d869a590b5..41f972be41af2176746f1005b5125e0a08df097a 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 48bee70f10396cb8cd2954b3661127c0ae850b6c..c6a13c06ce33490bc73173bedfaf1e9937a52bd7 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 78d61fe86d01e16431271ea5e8c92bc8a119c319..66c7b8a432e2c9447b802cf7483de153ca3325d3 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 c5483b3344fc283a590de535a6f5ef8c36ffdf64..8d571bbc63b99fe8027d90bed7c22f4ed68de305 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 035e9424e56c801b12f1a0dde230b8bac008f67e..edfda0592bee4a2045f09a0e36c28645de1f3323 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 00a46455801d7f05eae2636b9f2552ea9657984c..ea437fea72377575cb79f5e94b66d15069ea76c2 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 3ffca1fbf915ca88f3245b65d332d6311167d603..837d0e1e45e39930d1988a08e0ea07c88d6cfafa 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 26bec51fc8d92b184f7ef747b4943fafed591786..abe4e2eaa5c28c1f76b6ed2c50ced2141947ad41 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 b6d021225c8bce32b38a95048aad50bb2968a062..a06dc5733cb2cb7303a61440c613639371222cc6 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 e29631b8a5b21d0628fb15561736d3a283777832..cca69555c766f44169bb8771b08440057a5f6b68 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 d390eb1c4c28309b264e7e825e813dfef1f3f5e7..a950e14dff3503820cc8a879f886219ad78a0587 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 0c0cbf32dc17028704a44a6d64f957835b665310..fc7d050b24521121bdfa74244e53afd32a53181e 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 8a7c713c8d990f647ddc726d364e7cff7c40e54f..7fda7aacfb44417427237b67241e2bef198c8931 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 8cf00463c6abb4d538bfe217b023a85bde23dcf6..dd3fdd4f02d768a807738bffb1493ea9c4f621a3 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 14f55753e024cd9fb4db2467714678a7bca7e4f0..5b28df89d12ccbb8051e42b89182f03748ca1c81 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 9a3f5acfcf81edfdcf9520c327cc73182d931ea7..a2a55716573167c1fc15ef69d3151a01df0379a9 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 4574dca58e26aff403b7eb2159c1822a3f3f1e70..e82e9f80bc95edc796eeb435acf5ec890c3470e8 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 3d98232da6fb4b60a5fc5552915361dfda7911d0..a0df140af03e284fb0781bb76435bd931d208523 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 23b7c3ef79c3837ac3a62e2e3b190b11496664a7..6db4ffbbb3682482514466d0ca581b0cbcdcfed5 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 05e2cc6c2b23484f2a304af201ecd666368a47b5..f153e8ef24052c5a75baf9b393be4856f2df1065 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 f9b45f0464a214675c9b8698e81ec1e2c376a191..e0a5a2892c8ee7490dc6b1356d52096c6e255d12 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 3143486ccf9cd7375baf940dae08218991e4fcf7..5bde5408ebda31eed24aead1d36719d98329b936 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 927fb42244ec47729f38da804ba99574be5748ce..3ac8b39b8cf2548a44968d10c65ed1a5cf7dc6a0 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 0011d234b3176baf6e2bd31cb517018500c7545e..c6ccf1edd81197fdd2eaeb99f09f98a39d791e84 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 2976a5d41dc980772f5d3a79d880ad4c2c813aad..c6ed6fe5334d250995c3eac1f993d6b7cb0fca8e 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 402703114e8e08f47f5274ef118375c55a35cacd..a3c31a94f34f89517f38191f496905d5f25c88e0 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 1c6797ec843805fc64fa70610880940ffa559823..552baf18f481b50e62840e61835eaa641c81ac55 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 e965affde69abc80ba48c2963684508d1f0c920b..5a0720e59185214922a7d96229fab3893a78717c 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 6d38c76605f614622e01f7be5bd2bdb1869aae0d..5b88b1b5ee94e743d9dd21b550f568b973ba00b2 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 7a915ee9244dab7d311e44c1fdd98946f4f9a822..a3ab42af08ce18e1678368131ff7713b09d424e7 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 6d52e9a60c1d01005166ec53c5000456cd3d1a71..7fbd215298fc9f8c7ffb5c574449e25ec0341fb5 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 9db23a526861f867adb63cd5f40401c12c95f6a8..3d9c3603c93141ac10dd1366bd4975f229ee6a1c 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 0809775ec230e56165e6ce0b9017dbc578f2cfff..f8cd84605b3cdf668c94a28f037138f8e754afc1 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 09b8f74cfecb02848d515e4698f43443a2ca685a..688e0f7794693347d40ef947efb55909eb7ca83f 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 aced6216de9f5ed006d2c0bf3b2b3bb9769f9e4e..fce518bf744775cb7d095465090a0db91da5d2dc 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 75ef951bbd77353ea0736c7d4282511a8e041c8f..ec996d399ef5083f9e54141c2c37fc57e8ae72e6 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 14fe29dfd51491336cc7f2c969720b3b1e8386cb..0f6c45f066ffeabb956d3fcc852d0b061eff9b99 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 e81e71bb835c5f9c09c107b9b62699f4e901bd83..714614443f504dcf981613a14ccc7d33687e7f68 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 e176eb30039d854faaaca60a7607d2ed0274d364..7e7c76936f89caedc2c448c9173561d7280c2fbf 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 42ba8ee0393271fbe52bd88a082a78c2893c5c90..99d54f78cd8c4c109819c26a3acdafb2ab286f73 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 4589bb27c35efc511a456249ce0df415b66b8840..83b11f2a5b8c14c65d0ce128db0818c6256a7e31 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 b2aaa8ca69910cd07c5069c2dfc9c94b65501830..c60e8df3480e6bc04df4a3e3830182f2b211f048 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 af6ecb24015dfeb0761bc16d55d98e0b8c6d51f9..51511bf0d6f51a63e230af6d212c42c5a4cbf27a 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 aec94646f2bc3e86c2aa5abd574cf3a491c0323a..3b164f827c19117458569eefe0832e8258ab0548 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 4b288e5a5997816931b7fafb9b2d309413fd20d0..914f501d0adb1dfbbf2488d18489ff56d419a374 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 2e890742dff4898dddd4a7e91d2bb44f529fbc51..40ba06ea238e471ddf544cd77bfaea64dee4b57b 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 498fecbde1b6405f0716d1cf8f97741feaea97e3..aaf814b25772bb11ec894b0226acdb93f659212f 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 45566ba4b9fd5222cc467879b1914fb90fbabc12..3d3c507cc27500e340c48e3ac8b3338e2b74df91 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 fce86d47302aeb98bbce1d7a4bdb49ffe484c615..2d9aa5cc2636b0162c3d62fa7b174ef1db70b3e3 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 8a9d5d0e977bec0d7ff1ddbbf05dfa94e4e43e1a..3420216cf0df2e6aaaeda452b8e3aeaf23fecd87 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 bf091859e8251a2f7b188f8bd8c8b825282d2776..e291c2edf9bb1dd4f4c74b01e4af079fe467ff8a 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 4c53edb83d22f7e1f139e6288b7b825339ba0a9f..9411f0579b6f51eb6e79c6be9b283ce9eeb8d728 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 3f71579c9e0add91bd20a44d2e3e1b33a4d18d9c..37a00e2dfd2afbf89fc58d09ffbe55705f5ddedf 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 29bb525880633547308e2a932f10131a9674f27e..84a354edc1fa57cf3ca486fa9cbc513beb4ae452 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 6252de127270abae63484b1605e22f52029cc672..3e7c7b70d1583b24174e2242505e71bd58ffdf8e 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 3f71579c9e0add91bd20a44d2e3e1b33a4d18d9c..37a00e2dfd2afbf89fc58d09ffbe55705f5ddedf 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 f906c026ef6caafc7a3deac77cf3f4efea344b07..050a8decb88a8310f105f72929011010f3873e61 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 60ba0c8543e4393a9c6f06a2d4c286023af0d945..8e4de02ac336060c5c7f769c8d98d97f36b7c576 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 cb9c81ff71beb85725d1a13398bd9b2dbc0b4cb8..d3c6d2388e9d8ef541cc73ad03e60a2abcbcb9a5 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 f906c026ef6caafc7a3deac77cf3f4efea344b07..050a8decb88a8310f105f72929011010f3873e61 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 ed11ce892f134120960f0663b25c4b0e7f3b9a5f..119e6c19665d5d05d35cdfbea123a20404903b0d 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 ace6d99e2b8d8643db3e6de82c529ae80f7f5ca4..7d951c8eee7f58201342dd49a7b76121a1b92657 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 1f066a13bdf312687ff39faa8408687c6663e11a..80d9f13e6602b16ec2258a7669de447e5ba01f37 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 bf49288d17a7be3b22c66651a3dd44287c910518..091d6a168bd81721684630a13112db2d25a03fde 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 527d29bf4c0056a26f7f572cdf3298c729c291f1..4c2b21f458bf2d54325c7a6941cd74c1df396f24 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 15a0e39d7d53a017e39b238841f774a9b13505be..b8a6698a0e86d8b781851cef6e25d57f86d20f37 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 8de28af6ade5071ab1b9027e8b3553550f4c7595..7a0e25076663028e040169c7349da33754054aea 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 934205f9b85ace13d0d1128f32a14cfb334a6095..e63fa7c836730101b34a916509c262cb11a03120 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 8e6c0b02d5cd618f480523b59c5720b087e48e6e..8897170309d8a72e919748cb642896d7ec99d80d 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 347b37596a3d156fb44b1499459d1928e25b2c78..de399d3310c38e9cb824df1b5c3f5aebdf22796f 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 09e6d24bfb99f7884834118ce0d97d2fd2fb5074..0ab8412624e5e777072709dffa2768a0eb312245 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 d7a9b3eb5520fa0d07744db3d3897e047ebcb986..f374aa2c90d7dea2f00843fae1931ddb8c46392a 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 77a05fe96590e5f2f9669f5664af67e6eb9d22da..df650502cdfdc86f56d8eef102747cad78d759ea 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 f9551d56404c8647e903c8d8323584863bc2afa8..be1def0a2cb65a4c53f59765dc48ffa11437b87f 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 5da7a5e076271b86ebd3e8c4fc9a17bfda7a4e89..960aab00d4029f0adead3c539a3d00cb609d8def 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 168f4198a939e89a5926d77a6907c3be6836f16f..02e8c1d2360adb3839d0b8597fd8eab6a0e8b567 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 5da7a5e076271b86ebd3e8c4fc9a17bfda7a4e89..960aab00d4029f0adead3c539a3d00cb609d8def 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 6a64f8c02e0b8f8e50ada8a5b6cddb31e68de365..228d75d0793e6a057040ea309cdf1e5cf7882446 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 8186719bf9e387d08165eb044094d241c46b973f..16345d9fbaae1a8e53bd96e4ea4ab42a342b6176 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 5c186239a1ccdb1729862af4d12ea5a8e9912c03..cbd691bf6e8584ef05ac08a531636131747d283d 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 b772b0c964ba4735709ba3368f55888321c5c45b..be141b262f646d257e2daa311efb191ffc67aeec 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 9acc3334a83cebb4360301c0391f1986618b3752..bf2b31cf3f6536a00014e7b58fba655fe1f0c412 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 0d0bf54c3b22f30fde41b57cb43230eca1ed781d..61a15f0c7f9ad3d85d1c8c2b40624f9c13672eb1 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 165e3b25d522b0048f9f816fd1d7f5eb526edc63..3d47ca04c8e27fddcb54260b3386b62cecc619bc 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 44d0784d40a3bb8ec331ead38add541aa6735d6d..6680b30f53033ba6ff640f389c0891a4c92ea01f 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 fbda94034bccff059e600a74632b6956b7b8251a..80982aa02f37ddde5973c865edda4cb9e7994325 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 5c915be487aff71c83ffffac1b73213d44d96413..74f0a68aa9860513b8098b1edb00ac894f252647 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 44d0784d40a3bb8ec331ead38add541aa6735d6d..6680b30f53033ba6ff640f389c0891a4c92ea01f 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 60e1074500ab8fb6bca95f7806d299b44184c038..1886c4a5218b74f7c24ea0bcf2d6560863ae0960 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 1e4c64daf2c3feed7724e3b95ec294dbf4af6ffc..560729b7df8b3a8337832235eb147258088a54ee 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 3e1035f4dfd516b75089dc1531f52223a2d088a9..a03d25c63726834c877eeb39f76711d1f050b073 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 5b55f47494f1aed57085c83dbae9816200ec254e..736991532af28a1fa2321e2b3ca799caf087daf3 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 ->