diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index c42142c1..c94c5a5a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -294,8 +294,6 @@ jobs:
         with:
           node-version: 16
 
-      - run: echo "KRML_HOME=$(pwd)/karamel" >> $GITHUB_ENV
-
       - name: Karamel CI (test-pulse)
         working-directory: karamel
         run: |
diff --git a/test/pulse/Break.fst b/test/pulse/Break.fst
index 2b22a71b..61c03c00 100644
--- a/test/pulse/Break.fst
+++ b/test/pulse/Break.fst
@@ -9,12 +9,13 @@ fn simple_break ()
   while (!k)
     invariant live k
     ensures true
+    decreases (if !k then 1 else 0)
   {
     break;
   }
 }
 
-fn break_continue_and_return (which: UInt8.t)
+divergent fn break_continue_and_return (which: UInt8.t)
 {
   let mut i = 0ul;
   while (!i `UInt32.lt` 1000ul)
@@ -48,6 +49,7 @@ fn find_zero_with_break (a: array Int32.t) (sz: SizeT.t)
     invariant pure (SizeT.v !i <= SizeT.v sz /\
       (forall (j: nat). j < SizeT.v (!i) ==> Seq.index 'va j <> 0l))
     ensures (SizeT.v !i < SizeT.v sz /\ a.(!i) = 0l)
+    decreases (SizeT.v sz - SizeT.v (!i))
   {
     if (a.(!i) = 0l) {
       break;
diff --git a/test/pulse/Goto.fst b/test/pulse/Goto.fst
index e5bde886..1e1e30b0 100644
--- a/test/pulse/Goto.fst
+++ b/test/pulse/Goto.fst
@@ -29,6 +29,7 @@ fn find_zero (a: array Int32.t) (sz: SizeT.t)
     invariant live i
     invariant pure (SizeT.v !i <= SizeT.v sz /\
       (forall (j: nat). j < SizeT.v (!i) ==> Seq.index 'va j <> 0l))
+    decreases (SizeT.v sz - SizeT.v (!i))
   {
     if (a.(!i) = 0l) {
       return !i;
diff --git a/test/pulse/Inline.fst b/test/pulse/Inline.fst
index a79f9787..f9ff2a79 100644
--- a/test/pulse/Inline.fst
+++ b/test/pulse/Inline.fst
@@ -60,6 +60,8 @@ fn tst (shared : UInt32.t)
   let mut i = 0ul;
   while (!i <^ uu__k)
     invariant live i
+    invariant pure (v (!i) <= v uu__k)
+    decreases (Prims.op_Subtraction (v uu__k) (v (!i)))
   {
     i := !i +^ 1ul;
   };
diff --git a/test/pulse/InlineLoopCond.fst b/test/pulse/InlineLoopCond.fst
index fe47184f..96f326e8 100644
--- a/test/pulse/InlineLoopCond.fst
+++ b/test/pulse/InlineLoopCond.fst
@@ -3,7 +3,7 @@ module InlineLoopCond
 #lang-pulse
 open Pulse
 
-fn test (f : unit -> fn returns UInt32.t)
+divergent fn test (f : unit -> fn returns UInt32.t)
   returns UInt32.t
 {
   let uu__  = f ();
@@ -15,7 +15,7 @@ fn test (f : unit -> fn returns UInt32.t)
   0ul
 }
 
-fn test_ok (x : UInt32.t)
+divergent fn test_ok (x : UInt32.t)
   returns UInt32.t
 {
   (* This one could be inlined (it's not at the moment) *)