diff --git a/templates/svcomp_system_message.txt b/templates/svcomp_system_message.txt
index 3db3eb884..e1a13e5b0 100644
--- a/templates/svcomp_system_message.txt
+++ b/templates/svcomp_system_message.txt
@@ -22,6 +22,7 @@ Instructions:
     (iii) after the loop termination, 
     such that the loop invariants imply the post condition.
     - If a loop invariant is a conjunction, split it into its parts.
+    - If a variable does not change in the loop body, then output the equality of the variable with its value before the loop execution, as a loop invariant.
 - Output all the loop invariants and function contracts in one code block, with the corresponding labels as XML tags.
 Output each function contract in an XML tag of the form <Function_X>, where Function_X is the function label. Ensure each clause is in a separate line.
 Output each loop invariant in an XML tag of the form <Loop_X>, where Loop_X is the loop label.