diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
index 1cc37e8113c2e018354194b310ba91c89ce61a85..9799cadb813983e5a73c2fdc5844fa035b8beb34 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
@@ -44,6 +44,7 @@ type annotation_kind =
   | Precondition
   | Postcondition
   | Invariant
+  | Variant
   | RTE
 
 let kind_to_string loc k =
@@ -54,6 +55,7 @@ let kind_to_string loc k =
      | Precondition -> "Precondition"
      | Postcondition -> "Postcondition"
      | Invariant -> "Invariant"
+     | Variant -> "Variant"
      | RTE -> "RTE")
 
 let block stmt b = match b.bstmts with
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
index c56404a5a7120a2b752aacca94471f0c9f1ff758..4cdeb0fd23d1f0d62cb58b15806a3c321dc45c55 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
@@ -104,6 +104,7 @@ type annotation_kind =
   | Precondition
   | Postcondition
   | Invariant
+  | Variant
   | RTE
 
 val runtime_check: