diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 3d0c3cc4703562bfe215530fba8810c112a71d6c..6a09fa82d14c464eee53c17d2aeb9a284880fff1 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -496,6 +496,8 @@ struct
     let xs,tgs,domain,prop,_ =
       let cc_pred = pred `Positive in
       compile_step name types qs labels cc_pred in_pred prop in
+    let weak = Wp_parameters.WeakIntModel.get () in
+    let lemma = if weak then prop else F.p_hyps domain prop in
     {
       l_name = name ;
       l_types = List.length types ;
@@ -503,7 +505,7 @@ struct
       l_triggers = [tgs] ;
       l_forall = xs ;
       l_cluster = cluster ;
-      l_lemma = F.p_hyps domain prop ;
+      l_lemma = lemma ;
     }
 
   (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 8755b87107f3042d4e09bbe381fffafe685a2ae7..801be38dbfe47b4405249742bf21fa0632d45314 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -248,6 +248,14 @@ module Overflows =
                 (incompatible with RTE generator plug-in)"
   end)
 
+let () = Parameter_customize.set_group wp_model
+module WeakIntModel =
+  False(struct
+    let option_name = "-wp-weak-int-model"
+    let help = "Suppress integral type side conditions within lemmas\n\
+                (possibly unsound)"
+  end)
+
 let () = Parameter_customize.set_group wp_model
 module Literals =
   False(struct
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index fd0df0a2628df88f611165a8413c9b9dc33e2b5d..1543c5b56d939ade3398581dd4b5e7f4cf04a809 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -61,6 +61,7 @@ module InCtxt : Parameter_sig.String_set
 module ExternArrays: Parameter_sig.Bool
 module Literals : Parameter_sig.Bool
 module Volatile : Parameter_sig.Bool
+module WeakIntModel : Parameter_sig.Bool
 
 module Region: Parameter_sig.Bool
 module Region_rw: Parameter_sig.Bool