diff --git a/core/src/main/scala/stainless/genc/CPrinter.scala b/core/src/main/scala/stainless/genc/CPrinter.scala
index ae929ba2b..7a726bbb5 100644
--- a/core/src/main/scala/stainless/genc/CPrinter.scala
+++ b/core/src/main/scala/stainless/genc/CPrinter.scala
@@ -244,7 +244,9 @@ class CPrinter(
       }
 
     case Labeled(name, block) =>
-      c"""|$name:
+      // In C, a label cannot be followed by a variable declaration
+      // So we add a semicolon to add an empty statement to work around this
+      c"""|$name: ;
           |    $block"""
 
     case Lit(lit) => c"$lit"
diff --git a/frontends/benchmarks/genc/valid/TailRecAliasedArgs.scala b/frontends/benchmarks/genc/valid/TailRecAliasedArgs.scala
index b0ad1fc54..3eb743d71 100644
--- a/frontends/benchmarks/genc/valid/TailRecAliasedArgs.scala
+++ b/frontends/benchmarks/genc/valid/TailRecAliasedArgs.scala
@@ -4,6 +4,8 @@ import stainless.io._
 
 object TailRecAliasedArgs {
   def aliased(n: Int, a: Int, b: Int): Int =
+    require(n >= 0)
+    decreases(n)
     if n == 0 then a
     else aliased(n - 1, b, a + b)
 
diff --git a/frontends/benchmarks/genc/valid/TailRecComplexArgs.scala b/frontends/benchmarks/genc/valid/TailRecComplexArgs.scala
index 905b858f2..da9e08d01 100644
--- a/frontends/benchmarks/genc/valid/TailRecComplexArgs.scala
+++ b/frontends/benchmarks/genc/valid/TailRecComplexArgs.scala
@@ -4,6 +4,8 @@ import stainless.io._
 
 object TailRecComplexArgs {
   def complexArgs(n: Int): Int =
+    require(n >= 0)
+    decreases(n)
     if n <= 0 then 1
     else complexArgs(n - 1 * 2 + 1) // Complex argument
 
diff --git a/frontends/benchmarks/genc/valid/TailRecCountDown.scala b/frontends/benchmarks/genc/valid/TailRecCountDown.scala
index 540556122..9b414e6e1 100644
--- a/frontends/benchmarks/genc/valid/TailRecCountDown.scala
+++ b/frontends/benchmarks/genc/valid/TailRecCountDown.scala
@@ -4,6 +4,8 @@ import stainless.io._
 
 object TailRecNoArguments {
   def countDown(n: Int): Int =
+    require(n >= 0)
+    decreases(n)
     if n == 0 then 0
     else countDown(n - 1)
 
diff --git a/frontends/benchmarks/genc/valid/TailRecEarlyReturn.scala b/frontends/benchmarks/genc/valid/TailRecEarlyReturn.scala
index d65a271a4..444c565de 100644
--- a/frontends/benchmarks/genc/valid/TailRecEarlyReturn.scala
+++ b/frontends/benchmarks/genc/valid/TailRecEarlyReturn.scala
@@ -4,6 +4,8 @@ import stainless.io._
 
 object TailRecEarlyReturn {
   def earlyReturn(n: Int, acc: Int): Int =
+    require(n >= 0)
+    decreases(n)
     if n == 0 then acc
     else if n == 3 then return acc * 2 // Early return
     else earlyReturn(n - 1, acc + 1)
diff --git a/frontends/benchmarks/genc/valid/TailRecFib.scala b/frontends/benchmarks/genc/valid/TailRecFib.scala
index 231381af9..0c69bb746 100644
--- a/frontends/benchmarks/genc/valid/TailRecFib.scala
+++ b/frontends/benchmarks/genc/valid/TailRecFib.scala
@@ -5,6 +5,8 @@ import stainless.io._
 object TailRecFib {
 
   def fib(n: Int, i: Int = 0, j: Int = 1): Int =
+    require(n >= 0)
+    decreases(n)
     if n == 0 then i
     else fib(n-1, j, i+j)
 
diff --git a/frontends/benchmarks/genc/valid/TailRecFibAliased.scala b/frontends/benchmarks/genc/valid/TailRecFibAliased.scala
index 368371e70..6a2fdcf0c 100644
--- a/frontends/benchmarks/genc/valid/TailRecFibAliased.scala
+++ b/frontends/benchmarks/genc/valid/TailRecFibAliased.scala
@@ -5,6 +5,8 @@ import stainless.io._
 object TailRecFibAliased {
 
   def fib(n: Int, i: Int = 0, j: Int = 1): Int =
+    require(n >= 0)
+    decreases(n)
     if n == 0 then i
     else
         val res = fib(n-1, j, i+j)
diff --git a/frontends/benchmarks/genc/valid/TailRecMultipleCalls.scala b/frontends/benchmarks/genc/valid/TailRecMultipleCalls.scala
index df24cab93..0b6b6d6ab 100644
--- a/frontends/benchmarks/genc/valid/TailRecMultipleCalls.scala
+++ b/frontends/benchmarks/genc/valid/TailRecMultipleCalls.scala
@@ -4,7 +4,10 @@ import stainless.io._
 
 object TailRecMultipleCalls {
   def multipleCalls(n: Int, acc: Int): Int =
-    if n <= 0 then acc
+    require(n >= 0)
+    decreases(n)
+    if n == 0 then acc
+    else if n == 1 then acc + 2
     else if n % 2 == 0 then multipleCalls(n - 1, acc + 1)
     else multipleCalls(n - 2, acc + 2)
 
diff --git a/frontends/benchmarks/genc/valid/TailRecNested.scala b/frontends/benchmarks/genc/valid/TailRecNested.scala
index c538a03b7..b4063fec9 100644
--- a/frontends/benchmarks/genc/valid/TailRecNested.scala
+++ b/frontends/benchmarks/genc/valid/TailRecNested.scala
@@ -4,7 +4,10 @@ import stainless.io._
 
 object TailRecNested {
   def outer(n: Int): Int = 
+    require(n >= 0)
     def inner(x: Int): Int = 
+      require(x >= 0)
+      decreases(x)
       if x == 0 then 0
       else inner(x - 1)
     inner(n)
diff --git a/frontends/benchmarks/genc/valid/TailRecPatternMatching.check b/frontends/benchmarks/genc/valid/TailRecPatternMatching.check
index 62f945751..7813681f5 100644
--- a/frontends/benchmarks/genc/valid/TailRecPatternMatching.check
+++ b/frontends/benchmarks/genc/valid/TailRecPatternMatching.check
@@ -1 +1 @@
-6
\ No newline at end of file
+5
\ No newline at end of file
diff --git a/frontends/benchmarks/genc/valid/TailRecPatternMatching.scala b/frontends/benchmarks/genc/valid/TailRecPatternMatching.scala
index e2c6849d5..09c540424 100644
--- a/frontends/benchmarks/genc/valid/TailRecPatternMatching.scala
+++ b/frontends/benchmarks/genc/valid/TailRecPatternMatching.scala
@@ -3,14 +3,24 @@ import stainless.lang._
 import stainless.io._
 
 object TailRecPatternMatching {
-  def patternMatch(x: Option[Int], acc: Int): Int = x match
-    case None() => acc
-    case Some(0) => patternMatch(None(), acc + 1)
-    case Some(n) => patternMatch(Some(n - 1), acc + 1)
+  def patternMatch(x: Option[Int], acc: Int): Int = 
+    require(x match {
+      case None() => true
+      case Some(n) => n >= 1
+    })
+    val measure = x match {
+      case None() => 0
+      case Some(n) => n
+    }
+    decreases(measure)
+    x match
+      case None() => acc
+      case Some(n) if n == 1 => patternMatch(None(), acc + 1)
+      case Some(n) => patternMatch(Some(n - 1), acc + 1)
 
   @cCode.`export`
   def main(): Unit = {
     implicit val state = stainless.io.newState
-    StdOut.println(patternMatch(Some(5), 0)) // Expected: 6
+    StdOut.println(patternMatch(Some(5), 0)) // Expected: 5
   }
 }
diff --git a/frontends/benchmarks/genc/valid/TailRecReturnInLoop.check b/frontends/benchmarks/genc/valid/TailRecReturnInLoop.check
deleted file mode 100644
index 7c6ba0fe1..000000000
--- a/frontends/benchmarks/genc/valid/TailRecReturnInLoop.check
+++ /dev/null
@@ -1 +0,0 @@
-55
\ No newline at end of file
diff --git a/frontends/benchmarks/genc/valid/TailRecReturnInLoop.scala b/frontends/benchmarks/genc/valid/TailRecReturnInLoop.scala
deleted file mode 100644
index eff27125e..000000000
--- a/frontends/benchmarks/genc/valid/TailRecReturnInLoop.scala
+++ /dev/null
@@ -1,20 +0,0 @@
-import stainless.annotation._
-import stainless.lang._
-import stainless.io._
-
-object TailRecReturnInLoop {
-
-  def fib(n: Int, i: Int = 0, j: Int = 1): Int =
-    while (true) {
-      if n == 0 then return i
-      else return fib(n-1, j, i+j)
-    }
-    1
-
-  @cCode.`export`
-  def main(): Unit = {
-    implicit val state = stainless.io.newState
-    StdOut.println(fib(10))
-  }
-
-}
diff --git a/frontends/benchmarks/genc/valid/TailRecStackOverflow.scala b/frontends/benchmarks/genc/valid/TailRecStackOverflow.scala
index d489d0e9f..4f085bfbf 100644
--- a/frontends/benchmarks/genc/valid/TailRecStackOverflow.scala
+++ b/frontends/benchmarks/genc/valid/TailRecStackOverflow.scala
@@ -4,6 +4,8 @@ import stainless.io._
 
 object TailRecStackOverflow {
   def even(n: Int): Int =
+    require(n >= 0)
+    decreases(n)
     if n == 0 then 1
     else if n == 1 then 0
     else even(n - 2)
diff --git a/frontends/benchmarks/genc/valid/TailRecUnit.scala b/frontends/benchmarks/genc/valid/TailRecUnit.scala
index 6c7c7bf5a..82632eed3 100644
--- a/frontends/benchmarks/genc/valid/TailRecUnit.scala
+++ b/frontends/benchmarks/genc/valid/TailRecUnit.scala
@@ -4,6 +4,8 @@ import stainless.io._
 
 object TailRecUnit {
   def countDown(n: Int): Unit =
+    require(n >= 0)
+    decreases(n)
     if (n == 0) return
     countDown(n - 1)
 
diff --git a/frontends/benchmarks/genc/valid/TailRecUnitIf.scala b/frontends/benchmarks/genc/valid/TailRecUnitIf.scala
index babe23178..2aeba56e0 100644
--- a/frontends/benchmarks/genc/valid/TailRecUnitIf.scala
+++ b/frontends/benchmarks/genc/valid/TailRecUnitIf.scala
@@ -2,8 +2,10 @@ import stainless.annotation._
 import stainless.lang._
 import stainless.io._
 
-object TailRecUnit {
+object TailRecUnitIf {
   def countDown(n: Int): Unit =
+    require(n >= 0)
+    decreases(n)
     if (n == 0) return
     else countDown(n - 1)
 
diff --git a/frontends/benchmarks/genc/valid/TailRecUnitNoExplicitEnd.scala b/frontends/benchmarks/genc/valid/TailRecUnitNoExplicitEnd.scala
index 2cb60209d..1445e94e8 100644
--- a/frontends/benchmarks/genc/valid/TailRecUnitNoExplicitEnd.scala
+++ b/frontends/benchmarks/genc/valid/TailRecUnitNoExplicitEnd.scala
@@ -2,8 +2,10 @@ import stainless.annotation._
 import stainless.lang._
 import stainless.io._
 
-object TailRecUnit {
+object TailRecUnitWithNoExplicitEnd {
   def countDown(n: Int): Unit =
+    require(n >= 0)
+    decreases(n)
     if (n > 0) countDown(n - 1)
 
   @cCode.`export`