[wp] introduce weak int model for lemmas

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 ;
     }
 
   (* -------------------------------------------------------------------------- *)

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

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