From c866a933810ac60af33fe7ee386653da8d3d961c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 18 Sep 2020 14:15:28 +0200
Subject: [PATCH] [wp] updating qualif logs without driver

---
 src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle  | 1 -
 src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle   | 1 -
 .../wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle | 1 -
 .../wp/oracle_qualif/stmtcompiler_test_rela.res.oracle     | 1 -
 .../wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle        | 1 -
 .../wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle        | 1 -
 .../wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle       | 1 -
 src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle    | 1 -
 .../wp/tests/wp/oracle_qualif/wp_strategy.res.oracle       | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle      | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle      | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle | 1 -
 .../oracle_qualif/assigned_initialized_memtyped.res.oracle | 1 -
 .../oracle_qualif/assigned_initialized_memvar.res.oracle   | 1 -
 .../assigned_not_initialized_memtyped.res.oracle           | 1 -
 .../assigned_not_initialized_memvar.res.oracle             | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle | 1 -
 .../tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle | 1 -
 .../tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle       | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle  | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle      | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle     | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/boolean.res.oracle      | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/checks.res.oracle       | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle | 1 -
 .../wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle   | 1 -
 .../wp_acsl/oracle_qualif/classify_float.0.res.oracle      | 1 -
 .../wp_acsl/oracle_qualif/classify_float.1.res.oracle      | 1 -
 .../wp_acsl/oracle_qualif/classify_float.2.res.oracle      | 1 -
 .../wp_acsl/oracle_qualif/classify_float.3.res.oracle      | 1 -
 src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle  | 1 -
 src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle    | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle    | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle    | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle      | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/equal.res.oracle        | 1 -
 .../tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle | 1 -
 .../tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle  | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle   | 1 -
 .../wp_acsl/oracle_qualif/generalized_checks.res.oracle    | 1 -
 .../wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle    | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle   | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle | 1 -
 .../tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle  | 1 -
 .../wp_acsl/oracle_qualif/initialized_memtyped.res.oracle  | 1 -
 .../wp_acsl/oracle_qualif/initialized_memvar.res.oracle    | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle      | 1 -
 .../tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle | 1 -
 .../tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle  | 1 -
 .../tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle  | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/logic.res.oracle        | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle   | 1 -
 src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle    | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle    | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle  | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/range.res.oracle        | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle      | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle      | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle     | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle     | 1 -
 .../tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle   | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle       | 1 -
 .../wp_acsl/oracle_qualif/struct_use_case.0.res.oracle     | 1 -
 .../wp_acsl/oracle_qualif/struct_use_case.1.res.oracle     | 1 -
 src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle | 1 -
 .../tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle   | 1 -
 .../wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle    | 1 -
 .../wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle | 1 -
 .../wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle       | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle       | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts779.res.oracle        | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts788.res.oracle        | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts986.res.oracle        | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle      | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle      | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle      | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle      | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle      | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle      | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle      | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle    | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle    | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle      | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle      | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle      | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle    | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle    | 1 -
 .../wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle    | 1 -
 .../tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle   | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle     | 1 -
 .../tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle   | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle   | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle   | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle   | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle   | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle     | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle     | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle     | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle     | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle     | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_711.res.oracle     | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle   | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle   | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle     | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle     | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle      | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle     | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle     | 1 -
 .../wp/tests/wp_bts/oracle_qualif/issue_898.res.oracle     | 1 -
 .../tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle | 1 -
 .../binary-multiplication-without-overflow.res.oracle      | 1 -
 .../oracle_qualif/binary-multiplication.res.oracle         | 1 -
 .../wp/tests/wp_gallery/oracle_qualif/find.res.oracle      | 1 -
 .../oracle_qualif/frama_c_exo1_solved.res.oracle           | 1 -
 .../oracle_qualif/frama_c_exo2_solved.res.oracle           | 1 -
 .../oracle_qualif/frama_c_exo3_solved.old.res.oracle       | 1 -
 .../oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle    | 1 -
 .../frama_c_exo3_solved.simplified.res.oracle              | 1 -
 .../oracle_qualif/frama_c_hashtbl_solved.res.oracle        | 1 -
 .../wp_gallery/oracle_qualif/loop-statement.res.oracle     | 1 -
 .../oracle_qualif/alias_assigns_hypotheses.res.oracle      | 1 -
 .../wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle     | 1 -
 .../wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle     | 1 -
 .../tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle   | 1 -
 .../wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle      | 1 -
 .../wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle      | 1 -
 .../wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle     | 1 -
 .../wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle    | 1 -
 .../wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle    | 1 -
 .../wp_hoare/oracle_qualif/logicref_simple.res.oracle      | 1 -
 .../wp/tests/wp_hoare/oracle_qualif/reference.res.oracle   | 1 -
 .../wp_hoare/oracle_qualif/reference_and_struct.res.oracle | 1 -
 .../wp_hoare/oracle_qualif/reference_array.res.oracle      | 1 -
 .../oracle_qualif/reference_array_simple.res.oracle        | 1 -
 .../wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle   | 1 -
 .../wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle   | 1 -
 .../wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle   | 1 -
 .../wp/tests/wp_plugin/oracle/post_assigns.res.oracle      | 1 -
 .../wp/tests/wp_plugin/oracle/post_valid.res.oracle        | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle      | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle      | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle      | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/asm.res.oracle        | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle   | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/bool.res.oracle       | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle  | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle  | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/copy.res.oracle       | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle     | 1 -
 .../tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle | 1 -
 .../tests/wp_plugin/oracle_qualif/doomed_call.0.res.oracle | 1 -
 .../tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle | 1 -
 .../tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle | 1 -
 .../tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle | 1 -
 .../tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle | 1 -
 .../tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle   | 1 -
 .../wp_plugin/oracle_qualif/doomed_report_ko.res.oracle    | 1 -
 .../wp_plugin/oracle_qualif/doomed_report_ok.res.oracle    | 1 -
 .../tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle    | 1 -
 .../tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot | 1 +
 .../wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle   | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle    | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle    | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle    | 1 -
 .../wp_plugin/oracle_qualif/float_format.0.res.oracle      | 1 -
 .../wp_plugin/oracle_qualif/float_format.1.res.oracle      | 1 -
 .../wp_plugin/oracle_qualif/float_format.2.res.oracle      | 1 -
 .../tests/wp_plugin/oracle_qualif/float_real.0.res.oracle  | 1 -
 .../tests/wp_plugin/oracle_qualif/float_real.1.res.oracle  | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/frame.res.oracle      | 1 -
 .../tests/wp_plugin/oracle_qualif/ground_real.res.oracle   | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle  | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle | 1 -
 .../wp_plugin/oracle_qualif/init_const_guard.res.oracle    | 1 -
 .../tests/wp_plugin/oracle_qualif/init_extern.res.oracle   | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle    | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/loop.res.oracle       | 1 -
 .../tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle   | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle  | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle  | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/mask.res.oracle       | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/math.0.res.oracle     | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle     | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle     | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle     | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/model.res.oracle      | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle  | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle       | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/nth.res.oracle        | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle  | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/params.res.oracle     | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/plet.res.oracle       | 1 -
 .../tests/wp_plugin/oracle_qualif/post_assigns.res.oracle  | 7 +++++--
 .../wp/tests/wp_plugin/oracle_qualif/post_valid.res.oracle | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle     | 1 -
 .../tests/wp_plugin/oracle_qualif/region_to_coq.res.oracle | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/removed.res.oracle    | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle     | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/rte.res.oracle        | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle       | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle   | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/struct.res.oracle     | 1 -
 .../tests/wp_plugin/oracle_qualif/struct_hack.res.oracle   | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/subset.res.oracle     | 1 -
 .../tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle  | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/trig.res.oracle       | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle     | 1 -
 .../tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle | 1 -
 .../wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle   | 1 -
 .../wp/tests/wp_region/oracle_qualif/array1.res.oracle     | 1 -
 .../wp/tests/wp_region/oracle_qualif/array2.res.oracle     | 1 -
 .../wp/tests/wp_region/oracle_qualif/array3.res.oracle     | 1 -
 .../wp/tests/wp_region/oracle_qualif/array4.res.oracle     | 1 -
 .../wp/tests/wp_region/oracle_qualif/array5.res.oracle     | 1 -
 .../wp/tests/wp_region/oracle_qualif/array6.res.oracle     | 1 -
 .../wp/tests/wp_region/oracle_qualif/array7.res.oracle     | 1 -
 .../wp/tests/wp_region/oracle_qualif/array8.res.oracle     | 1 -
 .../wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle     | 1 -
 .../wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle    | 1 -
 .../wp/tests/wp_region/oracle_qualif/garbled.res.oracle    | 1 -
 .../wp/tests/wp_region/oracle_qualif/index.res.oracle      | 1 -
 .../wp/tests/wp_region/oracle_qualif/matrix.res.oracle     | 1 -
 .../tests/wp_region/oracle_qualif/structarray1.res.oracle  | 1 -
 .../tests/wp_region/oracle_qualif/structarray2.res.oracle  | 1 -
 .../tests/wp_region/oracle_qualif/structarray3.res.oracle  | 1 -
 .../tests/wp_region/oracle_qualif/structarray4.res.oracle  | 1 -
 .../wp/tests/wp_region/oracle_qualif/swap.res.oracle       | 1 -
 .../wp/tests/wp_store/oracle_qualif/array.res.oracle       | 1 -
 .../wp/tests/wp_store/oracle_qualif/natural.res.oracle     | 1 -
 .../tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle  | 1 -
 .../tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle  | 1 -
 .../wp/tests/wp_store/oracle_qualif/struct.res.oracle      | 1 -
 .../wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle  | 1 -
 .../wp_typed/oracle_qualif/array_initialized.0.res.oracle  | 1 -
 .../wp_typed/oracle_qualif/array_initialized.1.res.oracle  | 1 -
 .../wp/tests/wp_typed/oracle_qualif/avar.res.oracle        | 1 -
 .../wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle   | 1 -
 .../wp/tests/wp_typed/oracle_qualif/frame.res.oracle       | 1 -
 .../wp/tests/wp_typed/oracle_qualif/mvar.res.oracle        | 1 -
 .../wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle | 1 -
 .../wp_typed/oracle_qualif/struct_array_type.res.oracle    | 1 -
 .../tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle   | 1 -
 .../tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle   | 1 -
 .../tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle | 1 -
 .../tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle | 1 -
 .../wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle   | 1 -
 .../wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle   | 1 -
 .../wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle    | 1 -
 .../wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle  | 1 -
 .../wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle   | 1 -
 .../wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle    | 1 -
 .../wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle | 1 -
 .../wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle  | 1 -
 .../tests/wp_typed/oracle_qualif/unit_local.0.res.oracle   | 1 -
 .../tests/wp_typed/oracle_qualif/unit_local.1.res.oracle   | 1 -
 .../wp_typed/oracle_qualif/unit_loopscope.0.res.oracle     | 1 -
 .../wp_typed/oracle_qualif/unit_loopscope.1.res.oracle     | 1 -
 .../wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle | 1 -
 .../wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle | 1 -
 .../wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle   | 1 -
 .../tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle | 1 -
 .../tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle | 1 -
 .../tests/wp_typed/oracle_qualif/user_collect.res.oracle   | 1 -
 .../wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle | 1 -
 .../wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle | 1 -
 .../wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle | 1 -
 .../wp_typed/oracle_qualif/user_injector.0.res.oracle      | 1 -
 .../wp_typed/oracle_qualif/user_injector.1.res.oracle      | 1 -
 .../wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle    | 1 -
 .../wp/tests/wp_typed/oracle_qualif/user_string.res.oracle | 1 -
 .../wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle | 1 -
 .../wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle | 1 -
 .../wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle     | 1 -
 .../tests/wp_usage/oracle_qualif/caveat_range.res.oracle   | 1 -
 .../wp_usage/oracle_qualif/issue-189-bis.0.res.oracle      | 1 -
 .../wp_usage/oracle_qualif/issue-189-bis.1.res.oracle      | 1 -
 295 files changed, 6 insertions(+), 295 deletions(-)

diff --git a/src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle
index 783f051c009..0f4c53717a1 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp/cfg_loop.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 15 goals scheduled
 [wp] [Qed] Goal typed_loop_continue_loop_invariant_preserved : Valid
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle
index 7d5f6951348..94689205688 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp/sharing.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
index 6c7bce3b389..c396c4f4d7b 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
@@ -3,7 +3,6 @@
 [kernel] tests/wp/stmtcompiler_test.i:136: Warning: 
   Body of function if_assert falls-through. Adding a return statement
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [kernel] tests/wp/stmtcompiler_test.i:145: Warning: 
   No code nor implicit assigns clause for function behavior1, generating default assigns from the prototype
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle
index 6b7b63c6d93..85e1744ce20 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp/stmtcompiler_test_rela.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_empty_assert : Valid
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
index 83812560087..8fb43bd64b1 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-timeout 1 [...]
 [kernel] Parsing tests/wp/wp_behav.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] tests/wp/wp_behav.c:172: Warning: 
   Ignored specification 'for b1' (generalize to all behavior)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle
index 70bb96ddf24..5d374947a3c 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp/wp_behav.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] tests/wp/wp_behav.c:172: Warning: 
   Ignored specification 'for b1' (generalize to all behavior)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
index f27ec49d1b7..2da6874c320 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [kernel] tests/wp/wp_call_pre.c:53: Warning: 
   No code nor implicit assigns clause for function f, generating default assigns from the prototype
 [kernel] tests/wp/wp_call_pre.c:53: Warning: 
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle
index b91abd82765..11c277d30e4 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp/wp_eqb.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
index 505785f5e07..e630f56e9a5 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
@@ -9,7 +9,6 @@
 [rte] annotating function spec_if_cond
 [rte] annotating function spec_if_not_cond
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 25 goals scheduled
 [wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko1 : Unsuccess
 [wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko2 : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle
index 54afe789f74..7f14ed8bcd3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/arith.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 24 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_ASSOC_land_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle
index 8164480855d..414816fbfb3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp_acsl/arith.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_cast_sgn_usgn_ensures_qed_ko_KO : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle
index 5ec6a5228a3..09587f786aa 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/assign_array.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
 [wp] [Qed] Goal typed_jobA_assigns_exit : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle
index b2c5f9a9db3..4179df2cf6f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/assigned_initialized_memtyped.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 42 goals scheduled
 [wp] [Alt-Ergo] Goal typed_array_check_CHECK : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
index 45f96059729..bca9df7601c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/assigned_initialized_memvar.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 22 goals scheduled
 [wp] [Alt-Ergo] Goal typed_array_check_CHECK : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memtyped.res.oracle
index da65ee4ddd2..f95259fd614 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memtyped.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/assigned_not_initialized_memtyped.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 9 goals scheduled
 [wp] [Alt-Ergo] Goal typed_array_check_FAIL : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memvar.res.oracle
index d43006f651c..f7b59bf049b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memvar.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/assigned_not_initialized_memvar.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Alt-Ergo] Goal typed_array_check_FAIL : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
index a2e6ef5f8fb..180d946c317 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/assigns_path.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 9 goals scheduled
 [wp] [Qed] Goal typed_job_ensures_N : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle
index 12d57a19994..3cbb5dfd2f1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/assigns_range.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 17 goals scheduled
 [wp] [Qed] Goal typed_call_assigns_all_assigns_exit_part1 : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle
index d1cface46cf..18f62e7ca9b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp_acsl/assigns_range.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
 [wp] [Alt-Ergo] Goal typed_call_assigns_t1_assigns_exit : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle
index 2f3e2cbcff8..f2b749cff0c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/axioms.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 10 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_P_todo : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
index 365c8b069ca..a8fdef13518 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/base_offset.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Qed] Goal typed_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
index fe9cf947ab4..be66e97ea6a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/bitwise.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 29 goals scheduled
 [wp] [Qed] Goal typed_band_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle
index 722cd23bada..df621b7dc0c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/bitwise2.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 5 goals scheduled
 [wp] [Qed] Goal typed_job1_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle
index c366fd7097f..41e65885935 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/block_length.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 10 goals scheduled
 [wp] [Qed] Goal typed_f_ensures_Pt : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/boolean.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/boolean.res.oracle
index 9df0dc2a560..339f025ca51 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/boolean.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/boolean.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/boolean.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
 [wp] [Alt-Ergo] Goal typed_u8_is_continue_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle
index b4d2560332c..76d4cc6f9dd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 5 [...]
 [kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
 [wp] [Alt-Ergo] Goal typed_main_check_c1 : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
index 992ef461134..48e98d4fa14 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing tests/wp_acsl/chunk_typing.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [rte] annotating function function
 [wp] 39 goals scheduled
 [wp] [Alt-Ergo] Goal typed_function_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
index c503421c8a9..01ceab39f72 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing tests/wp_acsl/chunk_typing_usable.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [rte] annotating function usable_axiom
 [rte] annotating function usable_lemma
 [wp] Warning: native support for coq is deprecated, use tip instead
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle
index 80fb3297716..9d414c889b3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 3 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_InfN_not_finite : Valid
 [wp] [Alt-Ergo] Goal typed_lemma_InfP_not_finite : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
index bef955a1d64..e4946583721 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: native support for alt-ergo is deprecated, use why3 instead
 [wp] 3 goals scheduled
 [wp] [Alt-Ergo (native)] Goal typed_lemma_InfN_not_finite : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle
index f0c942664c1..4da1cb298a6 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 3 goals scheduled
 [wp] [Coq] Goal typed_lemma_InfN_not_finite : Saved script
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle
index b6583d3f4c6..6f5af142a49 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Real)' [...]
 [kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 3 goals scheduled
 [wp] [Qed] Goal typed_real_lemma_InfN_not_finite : Valid
 [wp] [Qed] Goal typed_real_lemma_InfP_not_finite : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
index 979b8b88f24..9ecfe8363f1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/cnf.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 43 goals scheduled
 [wp:cnf] CNF=P_A /\ P_A1 /\ P_A2
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle
index e9fd5565a05..8aa8444599f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/ctor.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 2 goals scheduled
 [wp] [Qed] Goal typed_lemma_cons : Valid
 [wp] [Qed] Goal typed_lemma_diff : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle
index 711ee91f78a..94777d12bef 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/div_mod.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 22 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_d0_div_pos_pos : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
index 711ee91f78a..94777d12bef 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/div_mod.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 22 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_d0_div_pos_pos : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle
index b798c16bdb6..65c66c6e2b9 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp_acsl/div_mod.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_d7_div_0_x_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle
index 7718ca4b67d..1f2b15cef67 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/e_imply.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 42 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_p0 : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle
index da11be9212d..da0936200fd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/equal.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
 [wp] [Alt-Ergo] Goal typed_simple_array_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle
index cb949a9f954..484d3489bb0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 19 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_finite_32_64 : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle
index 08e524f9e5a..37aaf32ef37 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Real)' [...]
 [kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 19 goals scheduled
 [wp] [Qed] Goal typed_real_lemma_finite_32_64 : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle
index bc8717807fd..a5148398dc4 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle
@@ -4,7 +4,6 @@
   Floating-point constant 0.1f is not represented exactly. Will use 0x1.99999a0000000p-4.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 8 goals scheduled
 [wp] [Alt-Ergo] Goal typed_double_convertible_check : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle
index d5aaa7c1240..538b5fb67c2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_acsl/funvar_inv.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Qed] Goal typed_ref_f_loop_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
index 4b3a0044393..f34b9052819 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-timeout 1 [...]
 [kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 17 goals scheduled
 [wp] [Alt-Ergo] Goal typed_check_lemma_C_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle
index 39d383ddb17..1d332c3eba2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/implicit_enum_cast.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 9 goals scheduled
 [wp] [Qed] Goal typed_bar_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
index 222fe3b9040..880080271e2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/init_label.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [kernel] tests/wp_acsl/init_label.i:27: Warning: 
   No code nor implicit assigns clause for function main, generating default assigns from the prototype
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
index 1fc7282684f..b396aef3b54 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/init_value.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 24 goals scheduled
 [wp] [Qed] Goal typed_fa1_ensures_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
index b790e806354..853a40b3b23 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp_acsl/init_value.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 18 goals scheduled
 [wp] [Alt-Ergo] Goal typed_fa1_ensures_qed_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle
index d5307168781..3cf52a8c985 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/init_value_mem.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_main_ensures_P : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
index 53fe740ee7b..11647c01b3d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/initialized_memtyped.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 28 goals scheduled
 [wp] [Alt-Ergo] Goal typed_formal_assert_provable : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
index ea40fb15e88..fa2acc12292 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/initialized_memvar.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 54 goals scheduled
 [wp] [Qed] Goal typed_globals_check_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle
index cf80df81df2..8bf8b806834 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/intbool.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_bug_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle
index 600fdf9a79b..e4c9550dc03 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/invalid_pointer.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_acsl/invalid_pointer.c:21: Warning: void object
 [wp] 19 goals scheduled
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle
index 43a22d025e2..f71b1ba16e1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/label_escape.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_g_assert_qed_ok_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle
index 6481802874a..fa9e50b10c4 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp_acsl/label_escape.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_f_assert_qed_ko_oracle_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
index 4f622671cdd..7c60acbc6bc 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/logic.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_acsl/logic.i:65: Warning: 
   Cast with incompatible pointers types (source: __anonstruct_Buint_4*)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle
index 492eb9634e0..c7494eb3cc7 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/looplabels.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 8 goals scheduled
 [wp] [Alt-Ergo] Goal typed_copy_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle
index c1a5e39bed0..1f8e9e47349 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/null.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_valid_non_null : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
index e84a81d1246..b078d29e165 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_acsl/pointer.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_acsl/pointer.i:50: Warning: 
   Uncomparable locations p_0 and mem:t.(0)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
index 89712b41fe4..a902f3f43d8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/pointer.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_acsl/pointer.i:50: Warning: 
   Uncomparable locations p_0 and mem:t.(0)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle
index e45ff82098c..d2eb8110c95 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp_acsl/post_result.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Qed] Goal typed_correct_assert_OK : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle
index ecfa8fc993b..b27efefadcd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle
@@ -37,7 +37,6 @@
 [kernel:annot-error] tests/wp_acsl/precedence.i:176: Warning: 
   P is not a logic variable. Ignoring code annotation
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 52 goals scheduled
 [wp] [Qed] Goal typed_bitwise_ensures_r_precedence_and_xor : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle
index 614ab582313..16f68c44ff1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle
@@ -37,7 +37,6 @@
 [kernel:annot-error] tests/wp_acsl/precedence.i:176: Warning: 
   P is not a logic variable. Ignoring code annotation
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 37 goals scheduled
 [wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_l_precedence_xor_and : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle
index c6b10dca91f..4d389265cd8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/range.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
 [wp] [Qed] Goal typed_test_ensures_P1_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle
index 6444362e5e2..9befe574b90 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/reads.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 7 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle
index 4d228ae7143..11234264105 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp_acsl/reads.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Alt-Ergo] Goal typed_modifies_x_ensures_qed_ko_G_KO : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle
index be665b9cca1..aafa831a5d6 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/record.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 11 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_M1_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle
index 6cf9ed0803c..9ee1634559a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp_acsl/record.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_KP5_qed_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
index 2f04de9548a..7db00e97afe 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/simpl_is_type.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 18 goals scheduled
 [wp] [Alt-Ergo] Goal typed_check_acsl_check_ok_C1_absurd_is_cint : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle
index 1e3debd8363..5eebd01bb77 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/sizeof.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_foo_assert_A : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle
index bc32b522fd6..3b8c905ab63 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Caveat)' [...]
 [kernel] Parsing tests/wp_acsl/struct_use_case.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_caveat_f_ensures_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle
index 692720f957a..f43f461d6c1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Caveat)' -wp-steps 50 [...]
 [kernel] Parsing tests/wp_acsl/struct_use_case.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_caveat_f_ensures_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle
index 6277a80bafa..bad7bc16a7c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/tset.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 4 goals scheduled
 [wp] [Qed] Goal typed_lemma_UNION_DESCR : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle
index 9b59b6bac5c..d891a566292 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/type_guard.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle
index 986a5310134..6cd53f6a5bb 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp_acsl/type_guard.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle
index f4ce0c5e623..d886facd8a8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/unit_bit_test.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
 [wp] [Qed] Goal typed_rotate_left_ensures_bit_zero : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle
index ebd003d69d4..6d9d902295d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/unit_bool.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 15 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_f_1 : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle
index 3eb172046e5..022b0364fa9 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/user_def_type_guard.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle
index a9b8d3dfbf9..0368f3b6126 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp_acsl/user_def_type_guard.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle
index 665ff4aed3b..2dd56ced052 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/bts0708.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_A : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
index af4c7b91ddd..fbd210f679c 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/bts0843.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
 [wp] [Qed] Goal typed_f3_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
index c5515d3585a..7f1e9b6e40f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing tests/wp_bts/bts779.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [rte] annotating function f
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_assert : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle
index 81c8416d16f..07263eaba24 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_bts/bts788.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Qed] Goal typed_ref_main_ensures_I0 : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle
index 03a9507ea81..8d3d1c250bf 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp_bts/bts986.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_f_assert_A : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle
index 5a020f66ee1..2cdd4e30969 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Real)' [...]
 [kernel] Parsing tests/wp_bts/bts_1174.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle
index abcda8d369d..e3b5535c1cb 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp_bts/bts_1176.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_f_assert_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle
index bf325fc4ff1..3472cd3cdfd 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing tests/wp_bts/bts_1360.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [rte] annotating function foo_correct
 [rte] annotating function foo_wrong
 [wp] 10 goals scheduled
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle
index 84c5b56ed46..0b3c861aaa9 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/bts_1462.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 13 goals scheduled
 [wp] [Qed] Goal typed_local_loop_invariant_preserved : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle
index 8f62c5605c8..5d88cb99d2c 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/bts_1586.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
 [wp] [Qed] Goal typed_compute_bizarre_Bizarre_ensures_TRANS : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle
index 5d175d94ffb..4b070090eaa 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/bts_1588.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_bts/bts_1588.i:19: Warning: 
   Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle
index 7efb8386c5f..86708cc7d79 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/bts_1601.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 8 goals scheduled
 [wp] [Alt-Ergo] Goal typed_foo_assert : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
index ebe06ce52f4..31ff857069f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/bts_1828.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
 [wp] [Alt-Ergo] Goal typed_global_frame_ensures_sep_iff_ref : Unsuccess
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
index 7e368e5770a..efbd5c95df3 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_bts/bts_1828.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
 [wp] [Qed] Goal typed_ref_global_frame_ensures_sep_iff_ref : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle
index 058efe3f4e9..c47673e6b51 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/bts_2040.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_call_assert : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle
index bfcb01c492d..6f837f71940 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/bts_2079.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Qed] Goal typed_main_ensures_Eval_P : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle
index afb849952b4..c02dc9c178f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/bts_2159.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_job_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle
index 75f2f1ffe20..99642408d02 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-timeout 1 [...]
 [kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_foo_assert_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
index 332bc081e7b..ffb3913bc38 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-timeout 1 [...]
 [kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: native support for alt-ergo is deprecated, use why3 instead
 [wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
index 50cddea1b70..daef8736024 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle
index 7c15d302575..abf5b969263 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/ergo_typecheck.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 8 goals scheduled
 [wp] [Qed] Goal typed_f_ensures_var_divded : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle
index 6fda3dfb53c..ea1d384da71 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue-364.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_main_assert_ZERO : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
index e1937ad2d56..be5d63c71f6 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue-684-exit.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
 [wp] [Qed] Goal typed_inconditional_exit_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle
index 485a5ed91f4..0f948292e59 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
 [wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
index 0e57e63b9d9..c34591c0821 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle
index 485a5ed91f4..0f948292e59 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
 [wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
index a4f2f3787a6..c4d6c3bd192 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 2 goals scheduled
 [wp] [Coq] Goal typed_lemma_ok_because_inconsistent : Default tactic
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle
index 6ab759c07bb..19ffd064dfc 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_198.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_broken : Valid
 [wp] Proved goals:    1 / 1
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle
index d5e25e1edd5..df5e033c97c 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_447.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_foo : Valid
 [wp] Proved goals:    1 / 1
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle
index c23bd61bb48..c4d33cc9b69 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_453.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
 [wp] [Qed] Goal typed_f1_loop_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle
index b4c5c4f4286..437f33f00c3 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_494.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle
index 72ff7aaa1bd..f5c735d0395 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_508.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Alt-Ergo] Goal typed_add_assigns_part1 : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_711.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_711.res.oracle
index ebb6855f35d..87633b0ea70 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_711.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_711.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_711.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_A : Valid
 [wp] Proved goals:    1 / 1
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle
index ed8d24a253a..2ab4a1454a9 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_715_a.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [kernel] tests/wp_bts/issue_715_a.i:6: Warning: 
   No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
index 9f9bc155c5f..694a10a84e8 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_715_b.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [kernel] tests/wp_bts/issue_715_b.i:9: Warning: 
   No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
index 300d4c7ea1f..6fc62ce363b 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_751.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 40 goals scheduled
 [wp] [Alt-Ergo] Goal typed_acquire_loop_invariant_RANGE_preserved : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle
index 338d948dadc..455278246bd 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_801.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
 [wp] [Qed] Goal typed_LoopCurrent_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle
index 9486ece4ecc..30935254772 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_81.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_getMax_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
index 35895046c31..cdf10ae7090 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_825.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 8 goals scheduled
 [wp] [Alt-Ergo] Goal typed_issue_check_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle
index 1e55e4e4da4..c8ec6fc55f2 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_837.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 9 goals scheduled
 [wp] [Qed] Goal typed_bar_assigns_part1 : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_898.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_898.res.oracle
index 7d9049804fb..9e1e9bcdbea 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_898.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_898.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/issue_898.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_job_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
index 272e07b8fe6..164271bc40a 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/nupw-bcl-bts1120.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] [CFG] Goal unreachable_smt_with_contract_assigns : Valid (Unreachable)
 [wp] [CFG] Goal unreachable_smt_with_contract_exits_ok : Valid (Unreachable)
 [wp] [CFG] Goal unreachable_smt_with_contract_ensures_ok : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
index 0c30eb6cf12..41402c7b8c2 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-rte -warn-unsigned-overflow [...]
 [kernel] Parsing tests/wp_gallery/binary-multiplication-without-overflow.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [rte] annotating function BinaryMultiplication
 [wp] 16 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_ax1_lack : Unsuccess
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
index 92bfb254ae4..c0a3091f89c 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing tests/wp_gallery/binary-multiplication.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [rte] annotating function BinaryMultiplication
 [wp] 17 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_ax4_ok : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
index c73a41611eb..f6155b9473b 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_gallery/find.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 41 goals scheduled
 [wp] [Qed] Goal typed_find_complete_found_not_found : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
index 6fc6f361576..e6750a21946 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_gallery/frama_c_exo1_solved.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 10 goals scheduled
 [wp] [Alt-Ergo] Goal typed_exo1_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
index bd27fc93329..5af041259b1 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_gallery/frama_c_exo2_solved.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 22 goals scheduled
 [wp] [Alt-Ergo] Goal typed_max_subarray_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
index 6d3d8657fd9..ee4bb865187 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.old.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 34 goals scheduled
 [wp] [Alt-Ergo] Goal typed_ref_equal_elements_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
index 0eb2143d7b4..e7d12e16b29 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.old.v2.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 35 goals scheduled
 [wp] [Alt-Ergo] Goal typed_ref_equal_elements_ensures_v1_good : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
index af7f5f6418e..c3667e36d84 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.simplified.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 26 goals scheduled
 [wp] [Qed] Goal typed_pair_complete_has_pair_no_pair : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
index 8e5320587c9..3d56522f9e5 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_gallery/frama_c_hashtbl_solved.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 102 goals scheduled
 [wp] [Alt-Ergo] Goal typed_add_complete_full_nominal : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle
index 206278a5b0a..bebcd6d2a22 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_gallery/loop-statement.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 15 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_Lb : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle
index 35b2ee5a8b5..cb72f2b3ee0 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_hoare/alias_assigns_hypotheses.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 30 goals scheduled
 [wp] [Qed] Goal typed_comprehension_alias_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle
index 056f3917be7..24386e88747 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_hoare/byref.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 12 goals scheduled
 [wp] [Qed] Goal typed_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle
index 0d4681981ee..447bc62e87d 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_hoare/byref.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 12 goals scheduled
 [wp] [Qed] Goal typed_ref_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
index 179a9259950..54ef16384aa 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_hoare/dispatch_var.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 78 goals scheduled
 [wp] [Qed] Goal typed_ref_array_in_struct_param_ensures_Pload2 : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle
index f2b9868fd88..54fb25c926c 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' -wp-no-let [...]
 [kernel] Parsing tests/wp_hoare/dispatch_var2.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 34 goals scheduled
 [wp] [Qed] Goal typed_ref_call_global_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle
index d23ba332da0..6601e9e2d00 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_hoare/dispatch_var2.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 34 goals scheduled
 [wp] [Qed] Goal typed_ref_call_global_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle
index dcf9b471da8..04d5a4f2629 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_hoare/isHoare.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_ref_cmp_invalid_addr_as_int_ensures_ok : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle
index cd7e781214b..efe1f7fdd17 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_hoare/logicarr.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Alt-Ergo] Goal typed_job_ensures_PTR : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle
index d2264fc7e59..1c127a17545 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_hoare/logicref.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 5 goals scheduled
 [wp] [Qed] Goal typed_ref_fvrange_n_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle
index 44f733dcecf..061f51954ca 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_hoare/logicref_simple.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 9 goals scheduled
 [wp] [Alt-Ergo] Goal typed_ref_fsimple_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
index e4be92ac66b..009b3d29625 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_hoare/reference.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 23 goals scheduled
 [wp] [Qed] Goal typed_ref_call_f2_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
index 757cef883b0..e29464dd555 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_hoare/reference_and_struct.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 32 goals scheduled
 [wp] [Qed] Goal typed_ref_call_array_in_struct_param_ensures_Pload2 : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
index edfb3c339c7..2d2721f7301 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_hoare/reference_array.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 36 goals scheduled
 [wp] [Alt-Ergo] Goal typed_ref_add_1_5_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle
index a53989661a5..b5390221da4 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_hoare/reference_array_simple.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Qed] Goal typed_ref_call_f1_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
index beca524545c..02a4bffe2c4 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_hoare/refguards.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 9 goals scheduled
 [wp] [Qed] Goal typed_ref_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle
index 676668f5c0a..213ee06d29f 100644
--- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle
+++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle
@@ -3,7 +3,6 @@
 [kernel] Parsing tests/wp_manual/working_dir/swap.c (with preprocessing)
 [kernel] Parsing tests/wp_manual/working_dir/swap1.h (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_swap_ensures_A : Valid
diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle
index 7eeef927165..4f1030ab270 100644
--- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle
+++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle
@@ -3,7 +3,6 @@
 [kernel] Parsing tests/wp_manual/working_dir/swap.c (with preprocessing)
 [kernel] Parsing tests/wp_manual/working_dir/swap2.h (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [rte] annotating function swap
 [wp] 8 goals scheduled
 [wp] [Alt-Ergo] Goal typed_swap_ensures_A : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
index 0a5c1608e7c..fc860528300 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/post_assigns.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 ------------------------------------------------------------
   Function receive
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/post_valid.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/post_valid.res.oracle
index ebeea945b1a..9848d7b4c8d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/post_valid.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/post_valid.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/post_valid.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 ------------------------------------------------------------
   Function job
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle
index 29ad79718d7..16adfa4946a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/abs.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_abs_abs_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle
index 1065fc610ec..3c71816dbbf 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/abs.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
index 3a68e2ef5e1..d5a8298ccca 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/abs.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: native support for alt-ergo is deprecated, use why3 instead
 [wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle
index 9548820aa57..344e6b07847 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/asm.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Qed] Goal typed_main_assert_OK : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle
index f6a082b42cc..fef95834e2e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/bit_test.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Alt-Ergo] Goal typed_bit_test_check1_ensures_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle
index 3d4c24ffb4a..d23de5bf36c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-no-let [...]
 [kernel] Parsing tests/wp_plugin/bool.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 7 goals scheduled
 [wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle
index 0f454d8c9dc..c58a574b23e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/convert.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_ceil : Valid
 [wp] [Alt-Ergo] Goal typed_lemma_floor : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
index 451f9a65769..e920dbe1256 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/convert.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: native support for alt-ergo is deprecated, use why3 instead
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo (native)] Goal typed_lemma_ceil : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle
index 8c4637944db..097475c27fe 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/copy.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 11 goals scheduled
 [wp] [Alt-Ergo] Goal typed_copy_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle
index a3d176c2b04..541ee8719f9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/doomed.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 7 goals scheduled
 [wp] [Passed] Smoke-test typed_bar_wp_smoke_default_requires
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle
index f11a3888e1d..dfc863b89cd 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/doomed_axioms.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 10 goals scheduled
 [wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_loop_s2
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.0.res.oracle
index 31663282840..0f1ab89f30e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/doomed_call.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 10 goals scheduled
 [wp] [Qed] Goal typed_f1_ok_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
index 3d349ae8897..1ccce739712 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/doomed_call.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 33 goals scheduled
 [wp] [Passed] Smoke-test typed_call_exit_ok_wp_smoke_dead_call_s2
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
index 51c6311db51..972512d6665 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-split [...]
 [kernel] Parsing tests/wp_plugin/doomed_call.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 36 goals scheduled
 [wp] [Passed] Smoke-test typed_call_exit_ok_wp_smoke_dead_call_s2
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
index 0b7ac571bbb..b256a09e43c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/doomed_dead.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 46 goals scheduled
 [wp] [Passed] Smoke-test typed_f1_ok_wp_smoke_dead_code_s3
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
index b5c0258a177..0b4390c4e11 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-split [...]
 [kernel] Parsing tests/wp_plugin/doomed_dead.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 48 goals scheduled
 [wp] [Passed] Smoke-test typed_f1_ok_wp_smoke_dead_code_s3
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle
index c1ea877c9ba..6cbe64cf0f1 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/doomed_loop.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 8 goals scheduled
 [wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_loop_s2
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
index 9daa85dfb61..4a65820f41c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/doomed_report_ko.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 10 goals scheduled
 [wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_loop_s2
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
index 2b80ca79ba3..c578928320d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/doomed_report_ok.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 10 goals scheduled
 [wp] [Passed] Smoke-test typed_foo_wp_smoke_dead_loop_s2
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle
index bcd42d15cb2..9f20f169f87 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/doomed_unroll.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_plugin/doomed_unroll.i:15: Warning: 
   Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
index a0f09e08be3..2561d69246c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/dynamic.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] tests/wp_plugin/dynamic.i:78: Warning: Missing 'calls' for default behavior
 [wp] Warning: Missing RTE guards
 [wp] 51 goals scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot b/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot
index adc97b189dd..7c51f93dabe 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot
@@ -35,6 +35,7 @@ digraph f {
   N100 [ color=green , label="Assume f_ensures_3" ] ;
  N100 -> N099 ;
   N101 [ color=red , label="Assigns f_assigns" ] ;
+  N101 -> N100 [ style=dotted ] ;
   N102 [ label="" , shape=circle ] ;
  N102 -> N101 ;
  N102 -> N100 ;
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
index 4b005c11a31..c78a7cf65a3 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/fallback.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.0.0'
 [wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle
index 219472265d9..0d5f90a7526 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-timeout 1 [...]
 [kernel] Parsing tests/wp_plugin/flash.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
 [wp] [Qed] Goal typed_job_ensures_Events : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle
index 70adda93016..a01eeba9e85 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/flash.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] tests/wp_plugin/flash-ergo.driver:2: Warning: 
   Redefinition of logic INDEX_init
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle
index 847a02d9f75..a87892007ee 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/flash.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
 [wp] [Qed] Goal typed_flash_job_ensures_Events : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
index beac21fa7b5..5ba66e74bab 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
@@ -4,7 +4,6 @@
   Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
index fd00d9ebd5b..0423017c2be 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
@@ -4,7 +4,6 @@
   Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: native support for alt-ergo is deprecated, use why3 instead
 [wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
index 5974584a73c..fcad25a085a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
@@ -4,7 +4,6 @@
   Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_output_ensures_KO : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle
index 96493d8e91a..265dcf74630 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle
@@ -4,7 +4,6 @@
   Floating-point constant 1e-5 is not represented exactly. Will use 0x1.4f8b588e368f1p-17.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_real_dequal_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle
index 497f15c885f..a42394bed4b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle
@@ -4,7 +4,6 @@
   Floating-point constant 1e-5 is not represented exactly. Will use 0x1.4f8b588e368f1p-17.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_dequal_ensures : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle
index 47c2b9e78e3..fb7fe232616 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/frame.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
 [wp] [Alt-Ergo] Goal typed_alias_ensures_KO : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle
index 9a35ec5ad1c..a875c26ce74 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/ground_real.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_R : Valid
 [wp] Proved goals:    1 / 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle
index 4c1700d30e3..6d7143512ed 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-timeout 240 [...]
 [kernel] Parsing tests/wp_plugin/inductive.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 2 goals scheduled
 [wp] [Coq] Goal typed_lemma_offset : Saved script
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle
index cdc1cc3b7c5..4389c814aec 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/init_const.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
 [wp] [Alt-Ergo] Goal typed_fA_ensures_KO : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle
index 21ceab5595d..2a606446dc5 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/init_const_guard.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 7 goals scheduled
 [wp] [Qed] Goal typed_f_ensures_Const : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle
index a998137dcc1..bbc0f9b1738 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle
@@ -2,7 +2,6 @@
 [kernel] Parsing tests/wp_plugin/init_extern.i (no preprocessing)
 [kernel] Parsing tests/wp_plugin/init_linker.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Qed] Goal typed_f_ensures_OK : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle
index 2ad8b725969..3f9234d02bd 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/init_valid.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
 [wp] [Qed] Goal typed_validA_assert_OK : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle
index 1654af3ba93..1607fa27193 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/initarr.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_job_ensures_SEP : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
index af35f6b8507..65ebd21fce6 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/injector.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 13 goals scheduled
 [wp] [Qed] Goal typed_f_call_g_requires : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle
index 273409a9bca..8730d221d29 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp_plugin/injector.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_ko_ensures_qed_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle
index 33f5a985986..602235b4e17 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/loop.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 9 goals scheduled
 [wp] [Alt-Ergo] Goal typed_init_ensures_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle
index 60ddf9009c6..75c868bd36a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/loopcurrent.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_plugin/loopcurrent.i:12: Warning: 
   Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle
index 93b40345adb..f62dda1b35e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/loopentry.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_plugin/loopentry.i:12: Warning: 
   Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle
index 32ed32900d4..111bb4a02c0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/loopextra.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_plugin/loopextra.i:6: Warning: 
   Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle
index fab459f7a10..a212cb8779f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/mask.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Qed] Goal typed_compute_ensures_A : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.0.res.oracle
index 82888040205..4af858324c1 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-timeout 100 -wp-steps 1500 [...]
 [kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 30 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_abs_neg : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
index a3c9e94c53e..40753d2a146 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-timeout 100 -wp-steps 1500 [...]
 [kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: native support for alt-ergo is deprecated, use why3 instead
 [wp] 30 goals scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
index 6dd9859b669..ffc737646cc 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-timeout 100 -wp-steps 10 [...]
 [kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 9 goals scheduled
 [wp] [Alt-Ergo] Goal typed_ko_ensures_ko_sin_asin : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
index 5b07b133292..81ba2360317 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-timeout 100 -wp-steps 10 [...]
 [kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: native support for alt-ergo is deprecated, use why3 instead
 [wp] 9 goals scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
index 45defe11c25..becab8e8f06 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
@@ -3,7 +3,6 @@
 [kernel] tests/wp_plugin/model.i:10: Warning: 
   parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 ---------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle
index 21dad7a45d6..d56af67a507 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/nosession.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Failed] Goal typed_f_ensures
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
index 28d3b1aac61..f11f92c390e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/nowp.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
index f7ef9322a99..1647eed4e12 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/nth.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 4 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_access_16_16_ok : Valid
 [wp] [Alt-Ergo] Goal typed_lemma_access_4_4_ok : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle
index a78f9d23cc2..6daeab38c98 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/overarray.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 12 goals scheduled
 [wp] [Qed] Goal typed_f1_ok_assigns_exit : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
index 5222a717ce6..5bfb2cf3e34 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/overassign.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 12 goals scheduled
 [wp] [Qed] Goal typed_f1_ok_assigns_exit : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle
index 66f2e22013f..f5af22f7014 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/params.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_lem : Valid
 [wp] Proved goals:    1 / 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle
index a8a6e9e1f36..30017bf15b0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/plet.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_GOAL : Valid
 [wp] Proved goals:    1 / 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle
index 0aace62366d..5f2225e888c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/post_assigns.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 5 goals scheduled
 [wp] [Qed] Goal typed_receive_ensures : Valid
@@ -16,5 +15,9 @@
   receive                   5        -        5       100%
 ------------------------------------------------------------
 [wp] Warning: Memory model hypotheses for function 'receive':
-  /*@ behavior typed: requires \separated(&size,message+(..)); */
+  /*@
+     behavior typed:
+       requires \separated(message + (..), &size);
+       requires \separated(message + (0 .. \at(size,Post)), &size);
+     */
   void receive(int n, char *message);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_valid.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_valid.res.oracle
index 7452d12d8c6..42883461442 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_valid.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_valid.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/post_valid.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Alt-Ergo] Goal typed_job_ensures_LOCAL : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle
index 522d782c44a..dcaa1de220c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/prenex.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 12 goals scheduled
 [wp] [Alt-Ergo] Goal typed_diag_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/region_to_coq.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/region_to_coq.res.oracle
index e9138f7b492..90915c00cf2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/region_to_coq.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/region_to_coq.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/region_to_coq.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 4 goals scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
index b622a45a0f7..2580c0129be 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
@@ -12,7 +12,6 @@
 [eva:final-states] Values at end of function main:
   __retres ∈ [-2147483647..2147483647]
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_main_assert_Eva_signed_overflow : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle
index 28ac3e50e6e..d2e67a0b560 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/repeat.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_plugin/repeat.c:47: Warning: 
   Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
index 71c6b6ffc4b..b15eec1d8c0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing tests/wp_plugin/rte.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [rte] annotating function job
 [rte] annotating function job2
 [rte] annotating function job3
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
index 64612393030..2be801f58b0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Caveat)' [...]
 [kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 39 goals scheduled
 [wp] [Qed] Goal typed_caveat_loops_ensures_ok_first : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
index 8905c23c28d..ad0100e7a0d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Caveat)' [...]
 [kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 34 goals scheduled
 [wp] [Qed] Goal typed_caveat_loops_ensures_ok_first : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
index b58e86cce5e..9f08e04867c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Caveat)' -wp-steps 50 [...]
 [kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle
index d9273f9a996..7bd29dc92c3 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/stmt.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] [CFG] Goal f_exits : Valid (Unreachable)
 [wp] [CFG] Goal g_exits : Valid (Unreachable)
 [wp] [CFG] Goal g_assigns : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle
index 0c67db7db87..e5ecf9b5e00 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-timeout 120 -wp-steps 2500 [...]
 [kernel] Parsing tests/wp_plugin/string_c.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 44 goals scheduled
 [wp] [Alt-Ergo] Goal typed_memcpy_ensures_copied_contents : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle
index 37e0be540b7..43fba563315 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/struct.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 18 goals scheduled
 [wp] [Qed] Goal typed_f_ensures_qed_ok_E0 : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle
index f42dd19bc62..15e36ca17c4 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle
@@ -3,7 +3,6 @@
 [kernel] tests/wp_plugin/struct_hack.i:46: Warning: 
   parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_plugin/struct_hack.i:37: Warning: 
   Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle
index 1330ec957e6..8fc2d073364 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/subset.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_mem_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle
index bc26d1ed0e5..7f76d80b00a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/subset_fopen.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 5 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_assert_Ok_A : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
index a4bc55ce426..59455952143 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/trig.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
 [wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_S : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
index e847532a8b0..1acc6c2f671 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/unroll.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_plugin/unroll.i:20: Warning: 
   Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle
index 2d2d4a2621c..6944a089a56 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/unsafe-arrays.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Qed] Goal typed_f_ensures_ARRAYS : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
index 1901df8a161..4dc2d8b6cab 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/unsigned.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 1 goal scheduled
 [wp] [Script] Goal typed_lemma_U32 : Valid
 [wp] Proved goals:    1 / 1
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle
index ed869315385..1af004f7352 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/array1.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle
index 5e7de78ee60..8a08fc00234 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/array2.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle
index d46d52bdc2c..1344cd80f93 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/array3.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle
index b732e6a34d5..cfd2596b059 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/array4.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle
index 31f6983483f..96c8bb9496d 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/array5.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle
index 34d7eb2a982..e9b4be282bb 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/array6.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle
index 0e0ad91c163..014de0bbb3a 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/array7.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle
index 13c02c6b2d1..c045da519b1 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/array8.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle
index 0db49291906..524115e64b4 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/fb_ADD.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle
index 372e798b673..98b5221f175 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/fb_SORT.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle
index af0aea662d2..7cae27dc0bb 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/garbled.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle
index fe16dc545ec..851c520b684 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/index.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle
index d0a1dcf567a..bd22d004dbb 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/matrix.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle
index 4f31df7dff8..f420eeb6427 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/structarray1.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle
index 94c1cbf1865..47409954b5b 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/structarray2.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle
index 0cee2a2b631..1acebc060c0 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/structarray3.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle
index 70c1d992d17..ec6b5a2de86 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/structarray4.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle
index 258e09a4a69..f736619caac 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_region/swap.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle
index 910812b95aa..9373264bf9d 100644
--- a/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_store/array.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Qed] Goal typed_g_ensures_P_startof_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle
index e2f8762967c..8d3b99ea687 100644
--- a/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_store/natural.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Qed] Goal typed_f_ensures_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle
index fd22abbbb9a..139e0d95e80 100644
--- a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_store/nonaliasing.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_qed_ok_P : Valid
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle
index bb918fb79e2..8d1a5b9cac9 100644
--- a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-steps 50 [...]
 [kernel] Parsing tests/wp_store/nonaliasing.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko_P_oracle_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle
index 461e3fcaa6f..344ab6e6f74 100644
--- a/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_store/struct.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
 [wp] [Qed] Goal typed_f_assert_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
index 0de1e597932..1fc22002b22 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_tip/tac_split_quantifiers.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 5 goals scheduled
 [wp] [Script] Goal typed_split_ensures_Goal_Exist_Or : Unsuccess
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle
index e2a176a72f5..0d1a283b5f8 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle
@@ -3,7 +3,6 @@
 [kernel] tests/wp_typed/array_initialized.c:13: Warning: 
   Too many initializers for array g
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 5 goals scheduled
 [wp] [Alt-Ergo] Goal typed_main1_assert : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle
index e2a176a72f5..0d1a283b5f8 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle
@@ -3,7 +3,6 @@
 [kernel] tests/wp_typed/array_initialized.c:13: Warning: 
   Too many initializers for array g
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 5 goals scheduled
 [wp] [Alt-Ergo] Goal typed_main1_assert : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle
index a9b513c05f6..878e590dd1e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/avar.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [kernel] tests/wp_typed/avar.i:4: Warning: 
   No code nor implicit assigns clause for function f, generating default assigns from the prototype
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle
index b720cb1e0e2..e706b784a7a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/cast_fits.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_typed/cast_fits.i:13: Warning: 
   Cast with incompatible pointers types (source: __anonstruct_L2_2*)
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle
index 2c002e7b1b1..dbc23301428 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/frame.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo] Goal typed_compound_assert_SEP : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
index 2d667089f84..65452ad8fe8 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/mvar.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [kernel] tests/wp_typed/mvar.i:14: Warning: 
   No code nor implicit assigns clause for function Write, generating default assigns from the prototype
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle
index e8a80395ed3..b09f19d9e21 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/shift_lemma.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 5 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_assert : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle
index 7513018dcd9..a7963a1a6f9 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/struct_array_type.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle
index 5e5b91dc94a..e3689c507d2 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_alloc.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 7 goals scheduled
 [wp] [Qed] Goal typed_f_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle
index 97a099bc62c..14f99e8e67f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_typed/unit_alloc.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 7 goals scheduled
 [wp] [Qed] Goal typed_ref_f_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle
index 03bc287592f..aa4dc3db059 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_bitwise.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 61 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_band_sint8 : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle
index 9c4dc9afa22..1c174b6ad2a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_bitwise.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
 [wp] [Alt-Ergo] Goal typed_band_int_assert_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle
index e39935873a6..e2091a07708 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_call.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [kernel] tests/wp_typed/unit_call.i:7: Warning: 
   No code nor implicit assigns clause for function f, generating default assigns from the prototype
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle
index 8d8d1eff5fc..c54e6f55894 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_cast.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_typed/unit_cast.i:4: Warning: 
   Cast with incompatible pointers types (source: sint32*) (target: sint8*)
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle
index 70fa445d32b..503a254a25f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_cst.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Qed] Goal typed_f_ensures_A : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle
index 6b5ca009e8d..df568124db5 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle
@@ -4,7 +4,6 @@
   Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
 [wp] [Qed] Goal typed_main_ensures_CST_F : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle
index 00ea955fe66..71e047a463e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_hard.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Qed] Goal typed_main_requires_p_is_33FF : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle
index 0bc63584c9b..0fc85faf32b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_ite.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_check_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle
index 802c3513d53..a255ecbfec3 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_labels.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Alt-Ergo] Goal typed_duplet_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle
index 6015427dddc..820a581c2e1 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_lemma.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] 6 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_P23_KO : Unsuccess
 [wp] [Alt-Ergo] Goal typed_lemma_P52 : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle
index ffa7b49597e..ab1c9992d7b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_local.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Qed] Goal typed_bar_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle
index 86474c5e363..131788981a3 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Raw)' [...]
 [kernel] Parsing tests/wp_typed/unit_local.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Alt-Ergo] Goal typed_raw_bar_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle
index 3b196114d45..80e267199ec 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_loopscope.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_typed/unit_loopscope.i:14: Warning: 
   Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
index 7e327b11a78..4417ddd127a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_typed/unit_loopscope.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_typed/unit_loopscope.i:14: Warning: 
   Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle
index 94ce30099a1..f48df3d43f6 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_matrix.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
 [wp] [Alt-Ergo] Goal typed_make_ensures_OK1 : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle
index 43b55a82a22..85998f35519 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_string.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_assert_AB : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle
index 756da0b5ce2..d82295e1dc5 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/unit_tset.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Qed] Goal typed_complex_call_job_requires : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle
index a29035c5b07..c210a11f4cc 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_typed/user_bitwise.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 12 goals scheduled
 [wp] [Qed] Goal typed_ref_rl1_ensures_b0 : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle
index ae33efb03cb..803894a6a5d 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_typed/user_bitwise.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
index ccc488ddf66..5e4efa11a65 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/user_collect.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 32 goals scheduled
 [wp] [Qed] Goal typed_caller_ensures_K : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
index a3eb99d5242..0ba543bbd4f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] [CFG] Goal init_exits : Valid (Unreachable)
 [wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
 [wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
index 3a972745592..757500ea677 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] [CFG] Goal init_exits : Valid (Unreachable)
 [wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
 [wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
index 21d17e27f81..ef421c4c808 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] [CFG] Goal init_exits : Valid (Unreachable)
 [wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
 [wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle
index d75c812e601..20fdb332cff 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/user_injector.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 20 goals scheduled
 [wp] [Qed] Goal typed_job_ensures_SEQ : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
index 90efeb24fce..93b4fb88899 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_typed/user_injector.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 16 goals scheduled
 [wp] [Qed] Goal typed_ref_job_ensures_SEQ : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle
index fdc05455b8d..16e16726067 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/user_rec.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 18 goals scheduled
 [wp] [Alt-Ergo] Goal typed_F1_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle
index 3b813077d9b..48d205c0e68 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/user_string.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 13 goals scheduled
 [wp] [Qed] Goal typed_strlen_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle
index dd19834fbb2..17290739f7c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_typed/user_swap.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 7 goals scheduled
 [wp] [Qed] Goal typed_main_assert : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
index 8b1b07121dc..258b04e2719 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Ref)' [...]
 [kernel] Parsing tests/wp_typed/user_swap.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
 [wp] [Qed] Goal typed_ref_main_assert : Valid
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
index f8365548e57..6c1a2b88219 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Caveat)' [...]
 [kernel] Parsing tests/wp_usage/caveat2.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] tests/wp_usage/caveat2.i:22: Warning: Undefined array-size (sint32[])
 [wp] 9 goals scheduled
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
index d985f8cbec7..050004166a7 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp -wp-model 'Typed (Caveat)' [...]
 [kernel] Parsing tests/wp_usage/caveat_range.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 12 goals scheduled
 [wp] [Alt-Ergo] Goal typed_caveat_reset_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle
index 1c5952f1a02..1aa3a66475c 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_usage/issue-189-bis.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 30 goals scheduled
 [wp] [Alt-Ergo] Goal typed_memcpy_alias_vars_ensures_memcpy : Valid
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
index 045de5e319b..c2679dccf0d 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_usage/issue-189-bis.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 10 goals scheduled
 [wp] [Alt-Ergo] Goal typed_memcpy_context_vars_ensures_memcpy_ok : Valid
-- 
GitLab