diff --git a/src/plugins/wp/MemVal.ml b/src/plugins/wp/MemVal.ml index 950f0518a5d6bdb957ce287173461d8501807962..bd41cf7b7c9cdb0958e6fb1d15e79cfed4cdd078 100644 --- a/src/plugins/wp/MemVal.ml +++ b/src/plugins/wp/MemVal.ml @@ -564,7 +564,8 @@ struct | _ -> load_loc ~assume:false sigma obj l end - let load_init _sigma _obj _loc = e_false + let load_init _sigma obj _loc = + e_var @@ Lang.freshvar ~basename:"i" @@ Lang.init_of_object obj (* -------------------------------------------------------------------------- *) (* --- Memory Store --- *)