diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala
index 70e0d7deb..c467ab0da 100644
--- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala
+++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala
@@ -105,7 +105,12 @@ trait StmtTyping extends BaseTyping { this: TypeInfoImpl =>
       }
       if (firstChecks.isEmpty) latterChecks else firstChecks
 
-    case n@PForStmt(_, cond, _, _, _) => isExpr(cond).out ++ comparableTypes.errors(exprType(cond), BooleanT)(n)
+    case n@PForStmt(_, cond, _, spec, _) =>
+      val isGhost = isEnclosingGhost(n)
+      val noTerminationMeasureMsg = "Loop occurring in ghost context does not have a termination measure"
+      isExpr(cond).out ++
+        comparableTypes.errors(exprType(cond), BooleanT)(n) ++
+        error(n, noTerminationMeasureMsg, isGhost && spec.terminationMeasure.isEmpty)
 
     case PShortForRange(range, shorts, _, _, _) =>
       underlyingType(exprType(range.exp)) match {
diff --git a/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra b/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra
index 4e5cd982c..21b06c68d 100644
--- a/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra
+++ b/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra
@@ -77,6 +77,7 @@ func ParallelSum(s []int) (res int) {
 		invariant forall j int :: 0 <= j && j < n ==> acc(&s[j], 1/2)
 		invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!>
 		invariant forall j int :: 0 <= j && j < n ==> (j < i ? acc(&seenSlice[j], 1/2) && seenSlice[j] == s[j] : sync.InjEval(tokens[j], j))
+		decreases n - i
 		for i:=0; i < n; i++ {
 			unfold sync.InjEval(tokens[i], i)
 			unfold locHasVal!<&seenSlice[i],s[i]!>()
diff --git a/src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra b/src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra
index 9942e04ed..82f22ddcd 100644
--- a/src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra
+++ b/src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra
@@ -127,6 +127,7 @@ func SearchReplace(s []int, x, y int) {
     invariant forall j int :: 0 <= j &&
       j < (i == len(seqs) ? len(s) : i * workRange) ==>
       acc(&s[j]) && s[j] == (s0[j] == x ? y : s0[j])
+    decreases len(pseqs) - i
     for i := 0; i != len(pseqs); i++ {
       unfold sync.InjEval(pseqs[i],i)
       low := i * workRange
diff --git a/src/test/resources/regressions/examples/evaluation/parallel_sum.gobra b/src/test/resources/regressions/examples/evaluation/parallel_sum.gobra
index 90357b532..9bd88a507 100644
--- a/src/test/resources/regressions/examples/evaluation/parallel_sum.gobra
+++ b/src/test/resources/regressions/examples/evaluation/parallel_sum.gobra
@@ -77,6 +77,7 @@ func ParallelSum(s []int) (res int) {
 		invariant forall j int :: 0 <= j && j < n ==> acc(&s[j], 1/2)
 		invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!>
 		invariant forall j int :: 0 <= j && j < n ==> (j < i ? acc(&seenSlice[j], 1/2) && seenSlice[j] == s[j] : sync.InjEval(tokens[j], j))
+		decreases n - i
 		for i:=0; i < n; i++ {
 			unfold sync.InjEval(tokens[i], i)
 			unfold locHasVal!<&seenSlice[i],s[i]!>()
diff --git a/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra b/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra
index f1c345a53..509af763d 100644
--- a/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra
+++ b/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra
@@ -128,6 +128,7 @@ func SearchReplace(s []int, x, y int) {
     invariant forall j int :: 0 <= j &&
       j < (i == len(seqs) ? len(s) : i * workRange) ==>
       acc(&s[j]) && s[j] == (s0[j] == x ? y : s0[j])
+    decreases len(pseqs) - i
     for i := 0; i != len(pseqs); i++ {
       unfold sync.InjEval(pseqs[i],i)
       low := i * workRange
diff --git a/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra b/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra
index 8faf2c427..dcec71c89 100644
--- a/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra
+++ b/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra
@@ -77,6 +77,7 @@ func ParallelSum(s []int) (res int) {
 		invariant forall j int :: 0 <= j && j < n ==> acc(&s[j], 1/2)
 		invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!>
 		invariant forall j int :: 0 <= j && j < n ==> (j < i ? acc(&seenSlice[j], 1/2) && seenSlice[j] == s[j] : sync.InjEval(tokens[j], j))
+		decreases n - i
 		for i:=0; i < n; i++ {
 			unfold sync.InjEval(tokens[i], i)
 			unfold locHasVal!<&seenSlice[i],s[i]!>()
diff --git a/src/test/resources/regressions/examples/parallel_search_replace_shared.gobra b/src/test/resources/regressions/examples/parallel_search_replace_shared.gobra
index 6d9a3f4dd..6fb31c82b 100644
--- a/src/test/resources/regressions/examples/parallel_search_replace_shared.gobra
+++ b/src/test/resources/regressions/examples/parallel_search_replace_shared.gobra
@@ -139,6 +139,7 @@ func SearchReplace(s []int, x, y int) {
     invariant forall j int :: 0 <= j &&
       j < (i == len(seqs) ? len(s) : i * workRange) ==>
       acc(&s[j]) && s[j] == (s0[j] == x ? y : s0[j])
+    decreases len(pseqs) - i
     for i := 0; i != len(pseqs); i++ {
       unfold sync.InjEval(pseqs[i],i)
       low := i * workRange
diff --git a/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra b/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra
index cf49e78b3..0dba9f06e 100644
--- a/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra
+++ b/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra
@@ -5,6 +5,9 @@ package pkg
 
 requires 0 < len(xs)
 func foo(ghost xs seq[bool]) {
-  //:: ExpectedOutput(for_loop_error:seq_index_exceeds_length_error)
-  ghost for ;xs[42]; { }
+  ghost {
+    decreases
+    //:: ExpectedOutput(for_loop_error:seq_index_exceeds_length_error)
+    for ;xs[42]; { break }
+  }
 }
diff --git a/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra b/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra
index eb0c91472..dbd56f595 100644
--- a/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra
+++ b/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra
@@ -5,6 +5,9 @@ package pkg
 
 requires 0 < len(xs)
 func foo(ghost xs seq[bool]) {
-  //:: ExpectedOutput(for_loop_error:seq_index_negative_error)
-  ghost for ;xs[-1]; { }
+  ghost {
+    decreases
+    //:: ExpectedOutput(for_loop_error:seq_index_negative_error)
+    for ;xs[-1]; { break }
+  }
 }
diff --git a/src/test/resources/regressions/features/sequences/seq-index-simple1.gobra b/src/test/resources/regressions/features/sequences/seq-index-simple1.gobra
index aa358a761..d8922779e 100644
--- a/src/test/resources/regressions/features/sequences/seq-index-simple1.gobra
+++ b/src/test/resources/regressions/features/sequences/seq-index-simple1.gobra
@@ -39,5 +39,8 @@ func example7(ghost xs seq[bool]) {
 
 requires 0 < len(xs)
 func example8(ghost xs seq[bool]) {
-  ghost for ;xs[0]; { }
+  ghost {
+    decreases
+    for ;xs[0]; { break }
+  }
 }
diff --git a/src/test/resources/regressions/issues/000796.gobra b/src/test/resources/regressions/issues/000796.gobra
new file mode 100644
index 000000000..d80945e9d
--- /dev/null
+++ b/src/test/resources/regressions/issues/000796.gobra
@@ -0,0 +1,20 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue000796
+
+func m1() {
+	//:: ExpectedOutput(type_error)
+	ghost for {
+		
+	}
+}
+
+func m2() {
+	ghost {
+		//:: ExpectedOutput(type_error)
+		for {
+		
+		}
+	}
+}
\ No newline at end of file