diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml
index b3a975d2a..f7ea6040d 100644
--- a/src/lustre/lustreAstNormalizer.ml
+++ b/src/lustre/lustreAstNormalizer.ml
@@ -83,9 +83,12 @@ type error = [
 
 type warning_kind = 
   | UnguardedPreWarning of A.expr
+  | UseOfAssertionWarning
 
 let warning_message warning = match warning with
   | UnguardedPreWarning expr -> "Unguarded pre in expression " ^ A.string_of_expr expr
+  | UseOfAssertionWarning ->
+    "Assertions are not checked; please consider using a contract assumption instead"
 
 type warning = [
   | `LustreAstNormalizerWarning of Lib.position * warning_kind
@@ -1047,6 +1050,7 @@ and normalize_contract info map items =
 and normalize_equation info map = function
   | Assert (pos, expr) ->
     let nexpr, map, warnings = abstract_expr true info map true expr in
+    let warnings = mk_warning pos UseOfAssertionWarning :: warnings in
     A.Assert (pos, nexpr), map, warnings
   | Equation (pos, lhs, expr) ->
     (* Need to track array indexes of the left hand side if there are any *)
diff --git a/src/lustre/lustreAstNormalizer.mli b/src/lustre/lustreAstNormalizer.mli
index 68841137e..d2f11ccdf 100644
--- a/src/lustre/lustreAstNormalizer.mli
+++ b/src/lustre/lustreAstNormalizer.mli
@@ -72,6 +72,7 @@ type error = [
 
 type warning_kind =
   | UnguardedPreWarning of LustreAst.expr
+  | UseOfAssertionWarning
 
 type warning = [
   | `LustreAstNormalizerWarning of Lib.position * warning_kind