Fist commit (WIP)

75 files changed, 396 insertions, 0 deletions

diff --git a/tests/sources/0000_noinit_var.c b/tests/sources/0000_noinit_var.c
new file mode 100644
index 0000000..6d1a0d4
--- /dev/null
+++ b/tests/sources/0000_noinit_var.c
@@ -0,0 +1 @@
+int x;
diff --git a/tests/sources/0001_noinit_2var.c b/tests/sources/0001_noinit_2var.c
new file mode 100644
index 0000000..2b9d16b
--- /dev/null
+++ b/tests/sources/0001_noinit_2var.c
@@ -0,0 +1,2 @@
+int x;
+int y;
diff --git a/tests/sources/0002_init_var.c b/tests/sources/0002_init_var.c
new file mode 100644
index 0000000..15bfa8f
--- /dev/null
+++ b/tests/sources/0002_init_var.c
@@ -0,0 +1 @@
+int x = 0;
diff --git a/tests/sources/0003_init_2var.c b/tests/sources/0003_init_2var.c
new file mode 100644
index 0000000..83aefaf
--- /dev/null
+++ b/tests/sources/0003_init_2var.c
@@ -0,0 +1,2 @@
+int x = 0;
+int y = 1;
diff --git a/tests/sources/0004_init_2var2.c b/tests/sources/0004_init_2var2.c
new file mode 100644
index 0000000..f81c09c
--- /dev/null
+++ b/tests/sources/0004_init_2var2.c
@@ -0,0 +1 @@
+int x = 9, y = 12;
diff --git a/tests/sources/0100_print_var.c b/tests/sources/0100_print_var.c
new file mode 100644
index 0000000..e2f9464
--- /dev/null
+++ b/tests/sources/0100_print_var.c
@@ -0,0 +1,2 @@
+int x = 2;
+print(x);
diff --git a/tests/sources/0101_print_2var.c b/tests/sources/0101_print_2var.c
new file mode 100644
index 0000000..92aa4a9
--- /dev/null
+++ b/tests/sources/0101_print_2var.c
@@ -0,0 +1,3 @@
+int x = 3;
+int y = 15;
+print(y);
diff --git a/tests/sources/0102_print_3var.c b/tests/sources/0102_print_3var.c
new file mode 100644
index 0000000..81fe534
--- /dev/null
+++ b/tests/sources/0102_print_3var.c
@@ -0,0 +1,4 @@
+int x = 3;
+int y = 15;
+int z = 99;
+print(z,x);
diff --git a/tests/sources/0103_local.c b/tests/sources/0103_local.c
new file mode 100644
index 0000000..c6683be
--- /dev/null
+++ b/tests/sources/0103_local.c
@@ -0,0 +1,5 @@
+int x = 12;
+{
+  int y = 9;
+  print(x,y);
+}
diff --git a/tests/sources/0200_assign_cst.c b/tests/sources/0200_assign_cst.c
new file mode 100644
index 0000000..8340469
--- /dev/null
+++ b/tests/sources/0200_assign_cst.c
@@ -0,0 +1,6 @@
+int x;
+print(x);
+x = 12;
+print(x);
+x = 15;
+print(x);
diff --git a/tests/sources/0201_assign_cst2.c b/tests/sources/0201_assign_cst2.c
new file mode 100644
index 0000000..6f28061
--- /dev/null
+++ b/tests/sources/0201_assign_cst2.c
@@ -0,0 +1,7 @@
+int x, y;
+print(x,y);
+x = 12;
+print(x,y);
+y = 15;
+x = 99;
+print(x,y);
diff --git a/tests/sources/0202_assign_expr.c b/tests/sources/0202_assign_expr.c
new file mode 100644
index 0000000..7d16636
--- /dev/null
+++ b/tests/sources/0202_assign_expr.c
@@ -0,0 +1,2 @@
+int x;
+x = 2 + 2;
diff --git a/tests/sources/0203_assign_expr2.c b/tests/sources/0203_assign_expr2.c
new file mode 100644
index 0000000..7583362
--- /dev/null
+++ b/tests/sources/0203_assign_expr2.c
@@ -0,0 +1,5 @@
+int x,y;
+x = 12;
+y = 16;
+x = x + y + 2;
+print(x);
diff --git a/tests/sources/0204_assign_rand.c b/tests/sources/0204_assign_rand.c
new file mode 100644
index 0000000..8bb9347
--- /dev/null
+++ b/tests/sources/0204_assign_rand.c
@@ -0,0 +1,3 @@
+int x;
+x = rand(1,99);
+print(x);
diff --git a/tests/sources/0205_assign_rand2.c b/tests/sources/0205_assign_rand2.c
new file mode 100644
index 0000000..a5aade7
--- /dev/null
+++ b/tests/sources/0205_assign_rand2.c
@@ -0,0 +1,3 @@
+int x;
+x = rand(10,-5);
+print(x);
diff --git a/tests/sources/0206_assign_add.c b/tests/sources/0206_assign_add.c
new file mode 100644
index 0000000..6c8dffe
--- /dev/null
+++ b/tests/sources/0206_assign_add.c
@@ -0,0 +1,2 @@
+int x;
+x = 2 + 5;
diff --git a/tests/sources/0207_assign_add2.c b/tests/sources/0207_assign_add2.c
new file mode 100644
index 0000000..1f8ec56
--- /dev/null
+++ b/tests/sources/0207_assign_add2.c
@@ -0,0 +1,2 @@
+int x; 
+x = rand(1,5) + rand (10,10);
diff --git a/tests/sources/0208_assign_add3.c b/tests/sources/0208_assign_add3.c
new file mode 100644
index 0000000..2f6357f
--- /dev/null
+++ b/tests/sources/0208_assign_add3.c
@@ -0,0 +1,2 @@
+int x;
+x = x + 2;
diff --git a/tests/sources/0209_assign_neg.c b/tests/sources/0209_assign_neg.c
new file mode 100644
index 0000000..f52fa2b
--- /dev/null
+++ b/tests/sources/0209_assign_neg.c
@@ -0,0 +1,2 @@
+int x;
+x = -9;
diff --git a/tests/sources/0210_assign_neg2.c b/tests/sources/0210_assign_neg2.c
new file mode 100644
index 0000000..d297b2c
--- /dev/null
+++ b/tests/sources/0210_assign_neg2.c
@@ -0,0 +1,3 @@
+int x;
+x = -rand(-1,10);
+
diff --git a/tests/sources/0211_assign_sub.c b/tests/sources/0211_assign_sub.c
new file mode 100644
index 0000000..8f7b962
--- /dev/null
+++ b/tests/sources/0211_assign_sub.c
@@ -0,0 +1,2 @@
+int x;
+x = 999 - 1;
diff --git a/tests/sources/0212_assign_sub2.c b/tests/sources/0212_assign_sub2.c
new file mode 100644
index 0000000..0b4f96f
--- /dev/null
+++ b/tests/sources/0212_assign_sub2.c
@@ -0,0 +1,2 @@
+int x;
+x = rand(1,10) - rand(2,3);
diff --git a/tests/sources/0213_assign_mul.c b/tests/sources/0213_assign_mul.c
new file mode 100644
index 0000000..6ba6b71
--- /dev/null
+++ b/tests/sources/0213_assign_mul.c
@@ -0,0 +1,2 @@
+int x; 
+x = 5 * 8;
diff --git a/tests/sources/0214_assign_mul2.c b/tests/sources/0214_assign_mul2.c
new file mode 100644
index 0000000..a5cdeef
--- /dev/null
+++ b/tests/sources/0214_assign_mul2.c
@@ -0,0 +1,2 @@
+int x;
+x = rand(1,3) * rand(2,9);
diff --git a/tests/sources/0215_assign_mul3.c b/tests/sources/0215_assign_mul3.c
new file mode 100644
index 0000000..b4affcf
--- /dev/null
+++ b/tests/sources/0215_assign_mul3.c
@@ -0,0 +1,2 @@
+int x;
+x = rand(-5,3) * rand(-1,10);
diff --git a/tests/sources/0216_assign_mul4.c b/tests/sources/0216_assign_mul4.c
new file mode 100644
index 0000000..7a10bb1
--- /dev/null
+++ b/tests/sources/0216_assign_mul4.c
@@ -0,0 +1,2 @@
+int x;
+x = x * 0;
diff --git a/tests/sources/0217_assign_copy.c b/tests/sources/0217_assign_copy.c
new file mode 100644
index 0000000..bdff7a4
--- /dev/null
+++ b/tests/sources/0217_assign_copy.c
@@ -0,0 +1,5 @@
+int x;
+int y;
+x = 12;
+y = x;
+print(y);
diff --git a/tests/sources/0218_assign_rel.c b/tests/sources/0218_assign_rel.c
new file mode 100644
index 0000000..921d6ec
--- /dev/null
+++ b/tests/sources/0218_assign_rel.c
@@ -0,0 +1,5 @@
+int x;
+int y;
+x = 15;
+y = x + 2;
+print(y);
diff --git a/tests/sources/0219_assign_rel2.c b/tests/sources/0219_assign_rel2.c
new file mode 100644
index 0000000..b19564d
--- /dev/null
+++ b/tests/sources/0219_assign_rel2.c
@@ -0,0 +1,3 @@
+int x = rand(1,5);
+int y = rand(2,10);
+int z = x + 2*y;
diff --git a/tests/sources/0300_if_true.c b/tests/sources/0300_if_true.c
new file mode 100644
index 0000000..c824dbc
--- /dev/null
+++ b/tests/sources/0300_if_true.c
@@ -0,0 +1,2 @@
+int x = 1;
+if (1 <= 2) x = 9;
diff --git a/tests/sources/0301_if_false.c b/tests/sources/0301_if_false.c
new file mode 100644
index 0000000..6ce93de
--- /dev/null
+++ b/tests/sources/0301_if_false.c
@@ -0,0 +1,2 @@
+int x = 1;
+if (1 >= 2) x = 9;
diff --git a/tests/sources/0302_if_both.c b/tests/sources/0302_if_both.c
new file mode 100644
index 0000000..5afc2f8
--- /dev/null
+++ b/tests/sources/0302_if_both.c
@@ -0,0 +1,2 @@
+int x = 1;
+if (rand(0,1) == 0) x = 9;
diff --git a/tests/sources/0303_if_else_true.c b/tests/sources/0303_if_else_true.c
new file mode 100644
index 0000000..8fa783f
--- /dev/null
+++ b/tests/sources/0303_if_else_true.c
@@ -0,0 +1,2 @@
+int x = 1;
+if (1 <= 2) x = 5; else x = 10;
diff --git a/tests/sources/0304_if_else_false.c b/tests/sources/0304_if_else_false.c
new file mode 100644
index 0000000..dab7fd2
--- /dev/null
+++ b/tests/sources/0304_if_else_false.c
@@ -0,0 +1,2 @@
+int x = 1;
+if (1 >= 2) x = 5; else x = 10;
diff --git a/tests/sources/0305_if_else_both.c b/tests/sources/0305_if_else_both.c
new file mode 100644
index 0000000..ddf0eb2
--- /dev/null
+++ b/tests/sources/0305_if_else_both.c
@@ -0,0 +1,2 @@
+int x = 1;
+if (rand(0,1) == 0) x = 5; else x = 10;
diff --git a/tests/sources/0306_if_rel.c b/tests/sources/0306_if_rel.c
new file mode 100644
index 0000000..66ddcc1
--- /dev/null
+++ b/tests/sources/0306_if_rel.c
@@ -0,0 +1,3 @@
+int x,y;
+if (rand(0,1) == 0) { x = 1; y = 3; }
+else { x = 2; y = 1; }
diff --git a/tests/sources/0307_if_var.c b/tests/sources/0307_if_var.c
new file mode 100644
index 0000000..a18b71b
--- /dev/null
+++ b/tests/sources/0307_if_var.c
@@ -0,0 +1,3 @@
+int x = rand(-10,20);
+if (x >= 0) { print(x); }
+else { print(x); }
diff --git a/tests/sources/0308_if_var2.c b/tests/sources/0308_if_var2.c
new file mode 100644
index 0000000..cf3aa0f
--- /dev/null
+++ b/tests/sources/0308_if_var2.c
@@ -0,0 +1,2 @@
+int x = rand(-20,10);
+if (x < 2) x = -x;
diff --git a/tests/sources/0309_if_var_rel.c b/tests/sources/0309_if_var_rel.c
new file mode 100644
index 0000000..1788f99
--- /dev/null
+++ b/tests/sources/0309_if_var_rel.c
@@ -0,0 +1,3 @@
+int x = rand(-10,25);
+int y = rand(-15,20);
+if (x >= y) x = y;
diff --git a/tests/sources/0310_cmp_le.c b/tests/sources/0310_cmp_le.c
new file mode 100644
index 0000000..5340ed4
--- /dev/null
+++ b/tests/sources/0310_cmp_le.c
@@ -0,0 +1,3 @@
+int x = rand(10,20);
+int y = rand(15,30);
+if (x <= y) print(x,y);
diff --git a/tests/sources/0311_cmp_le2.c b/tests/sources/0311_cmp_le2.c
new file mode 100644
index 0000000..d88fb3b
--- /dev/null
+++ b/tests/sources/0311_cmp_le2.c
@@ -0,0 +1,3 @@
+int x = rand(10,20);
+int y = rand(8,17);
+if (x <= y) print(x,y);
diff --git a/tests/sources/0312_cmp_le3.c b/tests/sources/0312_cmp_le3.c
new file mode 100644
index 0000000..00c4b32
--- /dev/null
+++ b/tests/sources/0312_cmp_le3.c
@@ -0,0 +1,3 @@
+int y = rand(10,20);
+int x = rand(30,55);
+if (x <= y) print(x);
diff --git a/tests/sources/0313_cmp_lt.c b/tests/sources/0313_cmp_lt.c
new file mode 100644
index 0000000..794fdd8
--- /dev/null
+++ b/tests/sources/0313_cmp_lt.c
@@ -0,0 +1,3 @@
+int x = rand(10,20);
+int y = rand(5,15);
+if (x < y) print(x,y);
diff --git a/tests/sources/0314_cmp_ge.c b/tests/sources/0314_cmp_ge.c
new file mode 100644
index 0000000..11ccae5
--- /dev/null
+++ b/tests/sources/0314_cmp_ge.c
@@ -0,0 +1,3 @@
+int x = rand(10,20);
+int y = rand(15,30);
+if (x >= y) print(x,y);
diff --git a/tests/sources/0315_cmp_gt.c b/tests/sources/0315_cmp_gt.c
new file mode 100644
index 0000000..2ab9e11
--- /dev/null
+++ b/tests/sources/0315_cmp_gt.c
@@ -0,0 +1,3 @@
+int x = rand(10,20);
+int y = rand(15,30);
+if (x > y) print(x,y);
diff --git a/tests/sources/0316_cmp_eq.c b/tests/sources/0316_cmp_eq.c
new file mode 100644
index 0000000..3fe7b2e
--- /dev/null
+++ b/tests/sources/0316_cmp_eq.c
@@ -0,0 +1,3 @@
+int x = rand(15,30);
+int y = rand(10,20);
+if (x == y) print(x,y);
diff --git a/tests/sources/0317_cmp_eq2.c b/tests/sources/0317_cmp_eq2.c
new file mode 100644
index 0000000..5d3b677
--- /dev/null
+++ b/tests/sources/0317_cmp_eq2.c
@@ -0,0 +1,3 @@
+int x = rand(15,20);
+int y = rand(25,30);
+if (x == y) print(x,y);
diff --git a/tests/sources/0318_cmp_ne.c b/tests/sources/0318_cmp_ne.c
new file mode 100644
index 0000000..8e7bf10
--- /dev/null
+++ b/tests/sources/0318_cmp_ne.c
@@ -0,0 +1,3 @@
+int x = rand(10,15);
+int y = rand(10,15);
+if (x != y) print(x,y);
diff --git a/tests/sources/0319_cmp_ne.c b/tests/sources/0319_cmp_ne.c
new file mode 100644
index 0000000..3dbe18b
--- /dev/null
+++ b/tests/sources/0319_cmp_ne.c
@@ -0,0 +1,3 @@
+int x = rand(10,15);
+int y = 10;
+if (x != y) print(x,y);
diff --git a/tests/sources/0320_cmp_eq_ne.c b/tests/sources/0320_cmp_eq_ne.c
new file mode 100644
index 0000000..6f4244c
--- /dev/null
+++ b/tests/sources/0320_cmp_eq_ne.c
@@ -0,0 +1,5 @@
+int x = rand(10,15);
+int y = 10;
+if (x == y) print(x,y);
+else print(x,y);
+
diff --git a/tests/sources/0321_cmp_rel.c b/tests/sources/0321_cmp_rel.c
new file mode 100644
index 0000000..d9c973c
--- /dev/null
+++ b/tests/sources/0321_cmp_rel.c
@@ -0,0 +1,3 @@
+int x = rand(10,20);
+int y = x;
+if (x >= 15) { print(y); }
diff --git a/tests/sources/0322_if_and.c b/tests/sources/0322_if_and.c
new file mode 100644
index 0000000..cd10203
--- /dev/null
+++ b/tests/sources/0322_if_and.c
@@ -0,0 +1,4 @@
+int x = rand(10,20);
+int y = rand(30,40);
+if (x>=15 && y>=35) { print(x,y); }
+else { print(x,y); }
diff --git a/tests/sources/0323_if_or.c b/tests/sources/0323_if_or.c
new file mode 100644
index 0000000..145983e
--- /dev/null
+++ b/tests/sources/0323_if_or.c
@@ -0,0 +1,4 @@
+int x = rand(10,20);
+int y = rand(30,40);
+if (x>=15 || y>=35) { print(x,y); }
+else { print(x,y); }
diff --git a/tests/sources/0324_if_not.c b/tests/sources/0324_if_not.c
new file mode 100644
index 0000000..8a6abb7
--- /dev/null
+++ b/tests/sources/0324_if_not.c
@@ -0,0 +1,4 @@
+int x = rand(10,20);
+int y = rand(30,40);
+if (!(x>=15) || y>=35) { print(x,y); }
+else { print(x,y); }
diff --git a/tests/sources/0325_if_bool.c b/tests/sources/0325_if_bool.c
new file mode 100644
index 0000000..614d5d7
--- /dev/null
+++ b/tests/sources/0325_if_bool.c
@@ -0,0 +1,4 @@
+int x = rand(10,20);
+int y = rand(10,20);
+if (x<=15 && y>=15 || x>=15 && y<=15) { print(x,y); }
+else { print(x,y); }
diff --git a/tests/sources/0400_assert_true.c b/tests/sources/0400_assert_true.c
new file mode 100644
index 0000000..6516bac
--- /dev/null
+++ b/tests/sources/0400_assert_true.c
@@ -0,0 +1,2 @@
+int x = 2;
+assert(x>=1);
diff --git a/tests/sources/0401_assert_false.c b/tests/sources/0401_assert_false.c
new file mode 100644
index 0000000..b2bc702
--- /dev/null
+++ b/tests/sources/0401_assert_false.c
@@ -0,0 +1,2 @@
+int x = 9;
+assert (x < 5);
diff --git a/tests/sources/0402_assert_both.c b/tests/sources/0402_assert_both.c
new file mode 100644
index 0000000..f9afd61
--- /dev/null
+++ b/tests/sources/0402_assert_both.c
@@ -0,0 +1,3 @@
+int x = rand (-5,10);
+assert(x >= 0);
+assert(x > 0);
diff --git a/tests/sources/0403_assert_both2.c b/tests/sources/0403_assert_both2.c
new file mode 100644
index 0000000..1a35775
--- /dev/null
+++ b/tests/sources/0403_assert_both2.c
@@ -0,0 +1,3 @@
+int x = rand (-5,10);
+assert(x > 0);
+assert(x >= 0);
diff --git a/tests/sources/0404_assert_rel.c b/tests/sources/0404_assert_rel.c
new file mode 100644
index 0000000..933d005
--- /dev/null
+++ b/tests/sources/0404_assert_rel.c
@@ -0,0 +1,4 @@
+int x,y;
+if (rand(0,1)==0) { x = 1; y = 1; }
+else { x = 3 ; y = 3; }
+assert(x==y);
diff --git a/tests/sources/0500_loop_count.c b/tests/sources/0500_loop_count.c
new file mode 100644
index 0000000..ace98cf
--- /dev/null
+++ b/tests/sources/0500_loop_count.c
@@ -0,0 +1,5 @@
+int x = 0;
+while (x < 100) {
+  print(x);
+  x = x + 1;
+}
diff --git a/tests/sources/0501_loop_infinite.c b/tests/sources/0501_loop_infinite.c
new file mode 100644
index 0000000..2676685
--- /dev/null
+++ b/tests/sources/0501_loop_infinite.c
@@ -0,0 +1,4 @@
+int x = 0;
+while (x < 10) {
+  print(x);
+}
diff --git a/tests/sources/0502_loop_infinite2.c b/tests/sources/0502_loop_infinite2.c
new file mode 100644
index 0000000..ef899a4
--- /dev/null
+++ b/tests/sources/0502_loop_infinite2.c
@@ -0,0 +1,5 @@
+int x = 0;
+while (x < 100) {
+  print(x);
+  x = x - 1;
+}
diff --git a/tests/sources/0503_loop_nondet.c b/tests/sources/0503_loop_nondet.c
new file mode 100644
index 0000000..ab17b7b
--- /dev/null
+++ b/tests/sources/0503_loop_nondet.c
@@ -0,0 +1,5 @@
+int x = 0;
+while (rand(0,1) == 0) {
+  print(x);
+  x = x + 1;
+}
diff --git a/tests/sources/0504_loop_rel.c b/tests/sources/0504_loop_rel.c
new file mode 100644
index 0000000..05804af
--- /dev/null
+++ b/tests/sources/0504_loop_rel.c
@@ -0,0 +1,7 @@
+int N = rand(0,1000);
+int x = 0;
+while (x < N) {
+  print(x,N);
+  x = x + 1;
+}
+assert(x==N);
diff --git a/tests/sources/0505_loop_rel2.c b/tests/sources/0505_loop_rel2.c
new file mode 100644
index 0000000..e335932
--- /dev/null
+++ b/tests/sources/0505_loop_rel2.c
@@ -0,0 +1,7 @@
+int N = rand(0,1000);
+int x = 0;
+while (x < N) {
+  print(x,N);
+  x = x + rand(0,3);
+}
+assert(x>=N && x<N+3);
diff --git a/tests/sources/0506_loop_limit.c b/tests/sources/0506_loop_limit.c
new file mode 100644
index 0000000..1a0d4f7
--- /dev/null
+++ b/tests/sources/0506_loop_limit.c
@@ -0,0 +1,5 @@
+int x = 0;
+while (rand(0,1)==0) {
+  if (x < 10000) x = x + 1;
+}
+print(x);
diff --git a/tests/sources/0507_loop_limit2.c b/tests/sources/0507_loop_limit2.c
new file mode 100644
index 0000000..bafdf77
--- /dev/null
+++ b/tests/sources/0507_loop_limit2.c
@@ -0,0 +1,6 @@
+int x = 0;
+int N = rand(0,1000);
+while (rand(0,1)==0) {
+  if (x < N) x = x + 1;
+}
+print(x);
diff --git a/tests/sources/0508_loop_init.c b/tests/sources/0508_loop_init.c
new file mode 100644
index 0000000..f0817e5
--- /dev/null
+++ b/tests/sources/0508_loop_init.c
@@ -0,0 +1,14 @@
+int init;
+int x;
+
+init = 0;
+while (rand(0,1)==0) {
+  if (init == 0) {
+    x = 0;
+    init = 1;
+  }
+  else {
+    x = x + 1;
+  }
+  assert(x >= 0);
+}
diff --git a/tests/sources/0509_loop_nested.c b/tests/sources/0509_loop_nested.c
new file mode 100644
index 0000000..54d5be6
--- /dev/null
+++ b/tests/sources/0509_loop_nested.c
@@ -0,0 +1,9 @@
+int i=0, j=0;
+
+while (i < 1000) {
+  j = 0;
+  while (j < i) {
+    j = j + 1;
+  }
+  i = i + 1;
+}
diff --git a/tests/sources/0510_loop_nested2.c b/tests/sources/0510_loop_nested2.c
new file mode 100644
index 0000000..90c52ec
--- /dev/null
+++ b/tests/sources/0510_loop_nested2.c
@@ -0,0 +1,10 @@
+int i,j;
+
+i = 0;
+while (i < 1000) {
+  j = 0;
+  while (j < i) {
+    j = j + 1;
+  }
+  i = i + 1;
+}
diff --git a/tests/sources/0600_bubble_sort.c b/tests/sources/0600_bubble_sort.c
new file mode 100644
index 0000000..5cad03d
--- /dev/null
+++ b/tests/sources/0600_bubble_sort.c
@@ -0,0 +1,32 @@
+// Example from Cousot Habwachs POPL 1978
+
+// Bubble sort, where array  operations are abstracted away
+// to get a non-deterministic scalar program
+
+// expected results:
+// - with polyhedra, no assertion failure (proof of absence of array overflow)
+// - with intervals, assertion failure
+
+int B,J,T;
+int N = rand(0,100000);  // array size
+
+B = N;
+while (B >= 1) {
+  J = 1;
+  T = 0;
+  while (J <= B-1) {
+
+    // array bound-check 
+    assert(1 <= J && J <= N);
+    assert(1 <= (J+1) && (J+1) <= N);
+
+    // the non-deterministic test models comparing TAB[J] and TAB[J+1]
+    if (rand(0,1)==0) {
+      // where, we would exchange TAB[J] and TAB[J+1];
+      T = J;
+    }
+
+    J = J + 1;
+  }
+  B = T;
+}
diff --git a/tests/sources/0601_heap_sort.c b/tests/sources/0601_heap_sort.c
new file mode 100644
index 0000000..dd12e1a
--- /dev/null
+++ b/tests/sources/0601_heap_sort.c
@@ -0,0 +1,66 @@
+// Example from Cousot Habwachs POPL 1978
+
+// Heap sort, where array  operations are abstracted away
+// to get a non-deterministic scalar program
+
+// expected results: with polyhedra, no assertion failure
+
+int L,R,I,J;
+int N = rand(1,100000);  // array size
+
+L = N/2 + 1;
+R = N;
+
+if (L >= 2) {
+  L = L - 1; 
+  // model the assignment "K = TAB[L]"
+  assert(1 <= L && L <= N);
+}
+else {
+  // model the assignments "K = TAB[R]; TAB[R] = TAB[1]"
+   assert(1 <= R && R <= N);
+   assert(1 <= 1 && 1 <= N);
+   R = R - 1;
+}
+
+while (R >= 2) {
+  I = L;
+  J = 2*I;
+
+  while (J <= R && rand(0,1)==0) {
+    if (J <= R-1) {
+      // model the comparison "TAB[J] < TAB[J+1]"
+      assert(1 <= J && J <= N);
+      assert(1 <= (J+1) && (J+1) <= N);
+      if (rand(0,1)==0) { J = J + 1; }
+    }
+
+    // model the comparison "K < TAB[J]"
+    assert(1 <= J && J <= N);
+    if (rand(0,1)==0) {
+      // model the assignment "TAB[I] = TAB[J]"
+      assert(1 <= I && I <= N);
+      assert(1 <= J && J <= N);   
+      I = J;
+      J = 2*J;
+    }
+  }
+
+  // model the assignment "TAB[I] = K"
+  assert(1 <= I && I <= N);
+
+  if (L >= 2) {
+    L = L - 1; 
+    // model the assignment "K = TAB[L]"
+    assert(1 <= L && L <= N);
+  }
+  else {
+    // model the assignments "K = TAB[R]; TAB[R] = TAB[1]"
+    assert(1 <= R && R <= N);
+    assert(1 <= 1 && 1 <= N);
+    R = R - 1;
+  }
+
+  // model the assignment "TAB[1] = K"
+  assert(1 <= 1 && 1 <= N);
+}
diff --git a/tests/sources/0602_rate_limiter.c b/tests/sources/0602_rate_limiter.c
new file mode 100644
index 0000000..a36da77
--- /dev/null
+++ b/tests/sources/0602_rate_limiter.c
@@ -0,0 +1,26 @@
+// Example from Miné HOSC 2006
+
+// Rate limiter: at each loop iteration, a new input is fetched (X) and
+// a new output (Y) is computed; Y tries to follow X but is limited to
+// change no more that a given slope (D) in absolute value
+
+// To prove that the assertion holds, this version needs the polyhedra
+// domain and an unrolling factor of at least 6
+
+int X;  // input
+int Y;  // output
+int S;  // last output
+int D;  // maximum slope;
+
+Y = 0;
+while (rand(0,1)==1) {
+  X = rand(-128,128);
+  D = rand(0,16);
+  S = Y;
+  int R = X - S; // current slope
+  Y = X;
+  if (R <= -D)     Y = S - D; // slope too small
+  else if (R >= D) Y = S + D; // slope too large
+}
+
+assert(Y >= -128 && Y <= 128);
diff --git a/tests/sources/0603_rate_limiter2.c b/tests/sources/0603_rate_limiter2.c
new file mode 100644
index 0000000..32a7a17
--- /dev/null
+++ b/tests/sources/0603_rate_limiter2.c
@@ -0,0 +1,21 @@
+// This version is similar to the previous one, but the assertion is checked
+// inside the loop
+// No unrolling is necessary in this version!
+
+int X;  // input
+int Y;  // output
+int S;  // last output
+int D;  // maximum slope;
+
+Y = 0;
+while (rand(0,1)==1) {
+  X = rand(-128,128);
+  D = rand(0,16);
+  S = Y;
+  int R = X - S; // current slope
+  Y = X;
+  if (R <= -D)     Y = S - D; // slope too small
+  else if (R >= D) Y = S + D; // slope too large
+
+  assert(Y >= -128 && Y <= 128);
+}