diff --git a/src/contracts/for_fail.ligo b/src/contracts/for_fail.ligo
new file mode 100644
index 000000000..0a177bca1
--- /dev/null
+++ b/src/contracts/for_fail.ligo
@@ -0,0 +1,11 @@
+// This was meant to test the for loop in PascaLIGO
+// But for whatever reason, the LIGO compiler currently thinks this is a 'complex loop'
+// even though it isn't. 
+// See this error:
+// $ ligo dry-run for.ligo main 0 0
+// bounded iterators: only simple for loops are supported yet 
+// {"loop_loc":"in file \"for.ligo\", line 4, characters 10-42"}
+
+
+function main (const a: int) : int is
+  block { for i := 0 to 100 block { skip } } with i;
diff --git a/src/contracts/procedure.ligo b/src/contracts/procedure.ligo
new file mode 100644
index 000000000..a0f6664c6
--- /dev/null
+++ b/src/contracts/procedure.ligo
@@ -0,0 +1,11 @@
+// Test a trivial PascaLIGO procedure
+
+procedure sub (const j: int) is 
+  begin
+    i := i + 1
+  end
+
+function main (const i: int) : int is 
+  begin 
+    sub(i)
+  end with i 
diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml
index 5380e9f0e..1b1a806cc 100644
--- a/src/passes/2-simplify/pascaligo.ml
+++ b/src/passes/2-simplify/pascaligo.ml
@@ -145,7 +145,7 @@ module Errors = struct
   let unsupported_for_loops region =
     let title () = "bounded iterators" in
     let message () =
-      Format.asprintf "only simple for loops are supported yet" in
+      Format.asprintf "only simple for loops are supported for now" in
     let data = [
       ("loop_loc",
        fun () -> Format.asprintf "%a" Location.pp_lift @@ region)
diff --git a/src/test/contracts/boolean_operators.ligo b/src/test/contracts/boolean_operators.ligo
index 4b53ff2d5..0d88c0f03 100644
--- a/src/test/contracts/boolean_operators.ligo
+++ b/src/test/contracts/boolean_operators.ligo
@@ -11,3 +11,6 @@ function and_true (const b : bool) : bool is
 
 function and_false (const b : bool) : bool is
   begin skip end with b and False
+
+function not_bool (const b: bool) : bool is
+  begin skip end with not b
diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo
index fcba9fda7..03cc751a7 100644
--- a/src/test/contracts/loop.ligo
+++ b/src/test/contracts/loop.ligo
@@ -7,7 +7,7 @@ function counter (var n : nat) : nat is block {
   }
 } with i
 
-function sum (var n : nat) : nat is block {
+function while_sum (var n : nat) : nat is block {
   var i : nat := 0n ;
   var r : nat := 0n ;
   while (i < n) block {
@@ -16,6 +16,13 @@ function sum (var n : nat) : nat is block {
   }
 } with r
 
+(* function for_sum (var n : nat) : nat is block {
+  for i := 1 to 100
+    begin 
+      n := n + 1;
+    end }
+  with n *)
+
 function dummy (const n : nat) : nat is block {
   while (False) block { skip }
 } with n
diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml
index 10d671050..172ab1c6e 100644
--- a/src/test/integration_tests.ml
+++ b/src/test/integration_tests.ml
@@ -15,6 +15,12 @@ let function_ () : unit result =
   let make_expect = fun n -> n in
   expect_eq_n_int program "main" make_expect
 
+(* Procedures are not supported yet 
+  let procedure () : unit result =
+  let%bind program = type_file "./contracts/procedure.ligo" in
+  let make_expect = fun n -> n + 1 in
+  expect_eq_n_int program "main" make_expect *)
+
 let assign () : unit result =
   let%bind program = type_file "./contracts/assign.ligo" in
   let make_expect = fun n -> n + 1 in
@@ -130,6 +136,7 @@ let bool_expression () : unit result =
       ("or_false", fun b -> b || false) ;
       ("and_true", fun b -> b && true) ;
       ("and_false", fun b -> b && false) ;
+      ("not_bool", fun b -> not b) ;
     ] in
   ok ()
 
@@ -529,10 +536,22 @@ let loop () : unit result =
   let%bind () =
     let make_input = e_nat in
     let make_expected = fun n -> e_nat (n * (n + 1) / 2) in
-    expect_eq_n_pos_mid program "sum" make_input make_expected
-  in
+    expect_eq_n_pos_mid program "while_sum" make_input make_expected
+  in(* For loop is currently unsupported 
+      
+  let%bind () = 
+    let make_input = e_nat in
+    let make_expected = fun n -> e_nat (n * (n + 1) / 2) in
+    expect_eq_n_pos_mid program "for_sum" make_input make_expected
+  in *)
   ok ()
 
+(* Don't know how to assert parse error happens in this test framework
+let for_fail () : unit result =
+  let%bind program = type_file "./contracts/for_fail.ligo" in
+  let%bind () = expect_fail program "main" (e_nat 0)
+  in ok () *)
+
 let matching () : unit result =
   let%bind program = type_file "./contracts/match.ligo" in
   let%bind () =
@@ -771,6 +790,7 @@ let website2_ligo () : unit result =
 let main = test_suite "Integration (End to End)" [
     test "type alias" type_alias ;
     test "function" function_ ;
+    (* test "procedure"  procedure ; *)
     test "assign" assign ;
     test "declaration local" declaration_local ;
     test "complex function" complex_function ;