diff --git a/headers/close-source/JCF_LGPL b/headers/close-source/JCF_LGPL
new file mode 100644
index 0000000000000000000000000000000000000000..040d941d8e378f0ad4cbfa0150f65e61eefe5435
--- /dev/null
+++ b/headers/close-source/JCF_LGPL
@@ -0,0 +1,12 @@
+
+Copyright (C) Jean-Christophe Filliatre
+
+This software is free software; you can redistribute it and/or
+modify it under the terms of the GNU Library General Public
+License version 2.1, with the special exception on linking
+described in file LICENSE.
+
+This software is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
+
diff --git a/headers/open-source/JCF_LGPL b/headers/open-source/JCF_LGPL
new file mode 100644
index 0000000000000000000000000000000000000000..169d635765b4441a4a98ee28a3c4c7b8e9e39c7e
--- /dev/null
+++ b/headers/open-source/JCF_LGPL
@@ -0,0 +1,15 @@
+
+Copyright (C) Jean-Christophe Filliatre
+
+This software is free software; you can redistribute it and/or
+modify it under the terms of the GNU Library General Public
+License version 2.1, with the special exception on linking
+described in file LICENSE.
+
+This software is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
+
+File modified by CEA (Commissariat à l'énergie atomique et aux
+                      énergies alternatives).
+
diff --git a/share/analysis-scripts/make_template.py b/share/analysis-scripts/make_template.py
index 94a6a8fe3ca393515bdaf624ea4ee6f4a10a9905..62ddb0080b0aad8c412059e7c1ca5d7827826fca 100755
--- a/share/analysis-scripts/make_template.py
+++ b/share/analysis-scripts/make_template.py
@@ -31,7 +31,7 @@ import re
 from subprocess import Popen, PIPE
 from pathlib import Path
 
-MIN_PYTHON = (3, 5) # for glob(recursive)
+MIN_PYTHON = (3, 6) # for glob(recursive) and automatic Path conversions
 if sys.version_info < MIN_PYTHON:
     sys.exit("Python %s.%s or later is required.\n" % MIN_PYTHON)
 
@@ -178,6 +178,7 @@ with open(sharedir / "analysis-scripts" / "template.mk") as f:
         check_path_exists("fc_stubs.c")
         from shutil import copyfile
         copyfile(sharedir / "analysis-scripts" / "fc_stubs.c", "fc_stubs.c")
+        lines = insert_line_after(lines, "^FCFLAGS", "  -main eva_main \\\n")
         print("Created stub for main function: fc_stubs.c")
 
 gnumakefile.write_text("".join(lines))
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 8a588c57c572b1219a59eb100a90ce3f13e7d188..c2b40db263f9920ee0586510e7ee3b68d3be4674 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -292,8 +292,8 @@ EACSL_DISTRIB_TESTS = \
   $(foreach dir, $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \
       $(dir)/*.[ich] \
       $(dir)/test_config \
-      $(dir)/oracle/*.c \
-      $(dir)/oracle/*.oracle \
+      $(dir)/oracle_ci/*.c \
+      $(dir)/oracle_ci/*.oracle \
   )
 
 EACSL_RTL_FILES = $(EACSL_RTL_SRC)
diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
index ed7dc106207e973679b8036711f40bc63f9292bc..1c3111811334a19ca77ff011c42803f7231edc2e 100644
--- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -46,17 +46,17 @@ compile the generated and the original (supplied) sources.
 By default no compilation is performed.
 .TP
 .B -D, --rt-debug
-Enable runtime debug features, i.e., compile unoptimized executable
+enable runtime debug features, i.e., compile unoptimized executable
 with assertions and extra checks.
 .TP
 .B --no-trace
-Disable stack trace reporting in debug mode
+disable stack trace reporting in debug mode
 .TP
 .B -V, --rt-verbose
-Output extra messages when executing generated code
+output extra messages when executing generated code
 .TP
 .B -X, --instrumented-only
-Do not compile original code. Has effect only in the presence of the \fI-c\fP
+do not compile original code. Has effect only in the presence of the \fI-c\fP
 flag.
 .TP
 .B -C, --compile-only
@@ -70,7 +70,7 @@ By default the -\fIdebug\fP flag is unused.
 pass a value to the \fBFrama-C\fP -\fIverbose\fP option.
 By default the -\fIverbose\fP flag is unused.
 .TP
-.B -V, --check
+.B --check
 check integrity of the generated AST (mostly useful for developers).
 .TP
 .B -o, --ocode=\fI<FILE>
@@ -157,25 +157,28 @@ Valid arguments are:
   \fIall\fP               \- all of the above.
 .TP
 .B -A, --rte-select=\fI<OPTSTRING>
-Restrict annotations to a given list of functions.
+restrict annotations to a given list of functions.
 \fIOPTSTRING\fP is a comma-separated string comprising function names.
 .TP
 .B --stack-size=\fI<NUMBER>
-Set the size (in MB) of the stack shadow space
+set the size (in MB) of the stack shadow space
 .TP
 .B --heap-size=\fI<NUMBER>
-Set the size (in MB) of the heap shadow space
+set the size (in MB) of the heap shadow space
 .TP
 .B -k, --keep-going
-Continue execution after an assertion failure
+continue execution after an assertion failure
 .TP
 .B --free-valid-address
-Trigger failure if a NULL-pointer is used as an input to free function
+trigger failure if a NULL-pointer is used as an input to free function
 .TP
 .B --fail-with-code=\fI<NUMBER>
-On assertion failure exit with the given integer code intead of raising an abort
+on assertion failure exit with the given integer code intead of raising an abort
 signal
 .TP
+.B --external-assert=\fI<FILE>
+the filename that contains your own implementation of __e_acsl_assert
+.TP
 .B -m, --memory-model=\fI<model>
 memory model (i.e., a runtime library for checking memory related annotations)
 to be linked against the instrumented file.
@@ -186,54 +189,58 @@ Valid arguments are:
 
 By default the Patricia trie  memory model is used.
 .TP
-.B --print-models
-Print the names of the supported memory models
+.B --print-mmodels
+print the names of the supported memory models
 .TP
 .B -I, --frama-c=\fI<FILE>
 the name of the \fBFrama-C\fP executable. By default the
 first \fIframa-c\fP executable found in the system path is used.
 .TP
+.B --e-acsl-share=\fI<DIR>
+the name of the \fBE-ACSL\fP share directory. If not provided, it is computed
+from your setting.
+.TP
 .B -G, --gcc=\fI<FILE>
 the name of the \fBGCC\fP executable. By default the first \fIgcc\fP
 executable found in the system path is used.
 .TP
 .B --then
-Separate with a \fB-then\fP the first \fBFrama-C\fP options from the actual
+separate with a \fB-then\fP the first \fBFrama-C\fP options from the actual
 launch of the \fBE-ACSL\fP plugin. Prepends \fB-e-acsl-prepare\fP to the list
 of options passed to \fBFrama-C\fP.
 .TP
 .B --e-acsl-extra=\fI<OPTS>
-Adds \fI<OPTS>\fP to the list of options that will be given to the \fBE-ACSL\fP
+add \fI<OPTS>\fP to the list of options that will be given to the \fBE-ACSL\fP
 analysis. Only useful when \fB--then\fP is in use, in which case \fI<OPTS>\fP
 will be placed after the \fB-then\fP on \fBFrama-C\fP's command-line. Otherwise,
 equivalent to \fB--frama-c-extra\fP
 .SH EXIT STATUS
 .TP
 .B 0
-Successful execution
+successful execution
 .TP
 .B 1
-Invalid user input
+invalid user input
 .TP
 .B \fBFrama-C\fP or \fBGCC\fP error code
-Instrumentation- or compile-time error
+instrumentation- or compile-time error
 
 .SH EXAMPLES
 
 .B e-acsl-gcc.sh foo.c
 
-Instrument foo.c and output the instrumented code to \fIa.out.frama.c\fP.
+instrument foo.c and output the instrumented code to \fIa.out.frama.c\fP.
 
 .B e-acsl-gcc.sh -P -c -ogen_foo.c -Ofoo foo.c
 
-Instrument \fIfoo.c\fP, output the instrumented code to \fIgen_foo.c\fP and
+instrument \fIfoo.c\fP, output the instrumented code to \fIgen_foo.c\fP and
 compile \fIfoo.c\fP into \fIfoo\fP and \fIgen_foo.c\fP into \fIfoo.e-acsl\fP.
 The \fB-P\fP option specifies that the instrumentation should omit debug
 functionality.
 
 .B e-acsl-gcc.sh --memory-model=bittree -C gen_foo.c
 
-Assume \fIgen_foo.c\fP has been instrumented by \fBE-ACSL\fP and compile it into
+assume \fIgen_foo.c\fP has been instrumented by \fBE-ACSL\fP and compile it into
 \fIa.out.e-acsl\fP using \fBbittree\fP memory model.
 
 .SH SEE ALSO
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
index 56f49d1a9d46970efcf0c5ef39c179969c342fd9..4e075e196a591c2729f55a6152d52ade99430459 100644
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
@@ -29,14 +29,20 @@ _eacsl_gcc() {
   prev="${COMP_WORDS[COMP_CWORD-1]}"
 
   opts="
-    -i -C -p -d -o -O -v -f -E -L -M -l -e -g -q -s -F -P -N -D -I -G -X -a
-    -h -c -msegment -mbittree
+    -i -C -p -d -o -O -v -V -f -E -L -M -l -e -g -q -s -F -P -N -D -I -G -X -a
+    -h -c -T -k
     --verbose= --debug= --debug-log= --logfile= --quiet --rt-debug --help
+    --rt-verbose --check --then --keep-going --fail-with-code --external-assert=
+    --no-trace
     --ocode= --oexec= --oexec-e-acsl=
     --ld-flags= --cpp-flags= --extra-cpp-args=
     --frama-c-extra= --frama-c= --gcc= --e-acsl-share= --memory-model=
-    --compile --compile-only --print --frama-c-only --instrumented-only
-    --gmp --full-mmodel --rte --no-int-overflow --no-stdlib --frama-c-stdlib"
+    --e-acsl-extra=
+    --compile --compile-only --print-mmodels --frama-c-only --instrumented-only
+    --gmp --full-mmodel --rte= --rte-select= --no-int-overflow
+    --no-stdlib --frama-c-stdlib --libc-replacements
+    --temporal --free-valid-address --weak-validity --validate-format-strings
+    --heap-size --stack-size"
 
   case ${prev} in
     -*)
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 3baaacb93aaaf2866e66c17dcc930b2de2d3cbd5..63cd1360942be5f6cda145a3a5e5b430bd788004 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -324,9 +324,11 @@ Usage: e-acsl-gcc.sh [options] files
 Options:
   -h         show this help page
   -c         compile instrumented code
+  -C         assume that the input files have already been instrumented
   -l         pass additional options to the linker
   -e         pass additional options to the prepreprocessor
   -E         pass additional arguments to the Frama-C preprocessor
+  -F         pass additional options to the Frama-C command line
   -p         output the generated code to STDOUT
   -o <file>  output the generated code to <file> [a.out.frama.c]
   -O <file>  output the generated executables to <file> [a.out, a.out.e-acsl]
diff --git a/src/plugins/gui/project_manager.ml b/src/plugins/gui/project_manager.ml
index 2e60e840184f5cee1e0b02eb2744304e7b43ffe3..d2f20659e5a19492ab859dc060a72019ce930d5a 100644
--- a/src/plugins/gui/project_manager.ml
+++ b/src/plugins/gui/project_manager.ml
@@ -251,7 +251,7 @@ and mk_project_entry window menu ?group p =
 
 and make_project_entries ?filter window menu =
   match projects_list ?filter () with
-  | [] -> assert false
+  | [] -> assert (filter <> None)
   | (pa, _name) :: tl ->
       let mk = mk_project_entry window menu in
       let pa_item = mk pa in
diff --git a/src/plugins/server/request.ml b/src/plugins/server/request.ml
index 01fd23fe22225c248c14dad8b62b96be6102b73f..0ec63893fbafe9db0c0617944fd5165fbd6efa8a 100644
--- a/src/plugins/server/request.ml
+++ b/src/plugins/server/request.ml
@@ -51,10 +51,7 @@ type 'a output = (module Output with type t = 'a)
 (* --- Sanity Checks                                                      --- *)
 (* -------------------------------------------------------------------------- *)
 
-let re_set = Str.regexp_string_case_fold "SET"
-let re_get = Str.regexp_case_fold "\\(GET\\|PRINT\\)"
-let re_exec = Str.regexp_case_fold "\\(EXEC\\|COMPUTE\\)"
-let re_name = Str.regexp_case_fold "[a-zA-Z0-9.]+$"
+let re_name = Str.regexp_case_fold "[a-zA-Z0-9._]+$"
 
 let wpage = Senv.register_warn_category "inconsistent-page"
 let wkind = Senv.register_warn_category "inconsistent-kind"
@@ -84,15 +81,6 @@ let check_page page name =
     Senv.warning ~wkey:wkind
       "Request '%s' shall not be published in protocol pages" name
 
-let check_kind kind name =
-  let re,key = match kind with
-    | `GET -> re_get , "get|print"
-    | `SET -> re_set , "set"
-    | `EXEC -> re_exec , "exec|compute"
-  in try ignore (Str.search_forward re name 0) with Not_found ->
-    Senv.warning "Request '%s' shall be named with « %s »"
-      name key
-
 (* -------------------------------------------------------------------------- *)
 (* --- Multiple Fields Requests                                           --- *)
 (* -------------------------------------------------------------------------- *)
@@ -256,7 +244,6 @@ let signature
     ~page ~kind ~name ~descr ?(details=[]) ?input ?output () =
   check_name name ;
   check_page page name ;
-  check_kind kind name ;
   let input = match input with None -> Pnone | Some d -> Pdata d in
   let output = match output with None -> Rnone | Some d -> Rdata d in
   {
diff --git a/src/plugins/server/syntax.ml b/src/plugins/server/syntax.ml
index 41d2b8e45ff7f87c49d5a57afaeba5f623be4da6..f36e96261b9656876d2da94ac9ab8ace01f35f46 100644
--- a/src/plugins/server/syntax.ml
+++ b/src/plugins/server/syntax.ml
@@ -30,7 +30,7 @@ let check_plugin plugin name =
   let k = String.length plugin in
   if not (String.length name > k &&
           String.sub n 0 k = p &&
-          String.get n k = '.')
+          String.get n k = '-')
   then
     Senv.warning ~wkey:Senv.wpage
       "Data %S shall be named « %s-* »"
diff --git a/src/plugins/value/utils/value_results.ml b/src/plugins/value/utils/value_results.ml
index 4363193a1b51f6a8de4275dde0e0a23aa1f4434e..d82bc2853b2e0ab84a0d2998efa46bbfa702b833 100644
--- a/src/plugins/value/utils/value_results.ml
+++ b/src/plugins/value/utils/value_results.ml
@@ -498,7 +498,8 @@ let make_report ()  =
   let report = empty_report () in
   let report_property ip =
     match ip with
-    | Property.IPCodeAnnot {Property.ica_ca} ->
+    | Property.IPCodeAnnot Property.{ ica_ca; ica_stmt; }
+      when Db.Value.is_reachable_stmt ica_stmt ->
       begin
         let status = get_status ip in
         match Alarms.find ica_ca with
@@ -506,11 +507,13 @@ let make_report ()  =
         | Some alarm ->
           let acc_status, acc_alarms = report.alarms in
           report_status acc_status status;
-          report_alarm acc_alarms alarm
+          match status with
+          | None | Some Property_status.True -> ()
+          | _ -> report_alarm acc_alarms alarm
       end
-    | Property.IPPropertyInstance _ ->
-      let status = get_status ip in
-      report_status report.preconds status
+    | Property.IPPropertyInstance {Property.ii_stmt}
+      when Db.Value.is_reachable_stmt ii_stmt ->
+      report_status report.preconds (get_status ip)
     | _ -> ()
   in
   Property_status.iter report_property;
diff --git a/src/plugins/wp/Auto.ml b/src/plugins/wp/Auto.ml
index eafe23bd7bae4684b87673ef80e6e94e983cdde6..38a8abc359dc4023ec95d78fb48c98b094949e76 100644
--- a/src/plugins/wp/Auto.ml
+++ b/src/plugins/wp/Auto.ml
@@ -85,7 +85,11 @@ let t_range e a b ~upper ~lower ~range s =
   ]
 
 let t_replace ?(equal="equal") ~src ~tgt (pi : Tactical.process) s =
-  let s' = Conditions.subst (fun e -> if e == src then tgt else e) s in
+  let s' =
+    Conditions.subst
+      (fun e -> if e == src then tgt else raise Not_found)
+      s
+  in
   (equal , (fst s, p_equal src tgt)) :: (pi s')
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index df462a66c69f15e9791099eb4dbb13fc9a9ad698..94248faed18a00b9d3e6ef53a09588f184621420 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -28,7 +28,20 @@ Plugin WP 20.0 (Calcium)
 - Gui         [2019/09/17] Updated panel for provers, models, cache, etc.
 - WP          [2019/09/12] New cache mechanism for why3 provers, see -wp-cache option
 -! WP         [2019/09/17] Deprecated native alt-ergo & coq output, see -wp-prover option
--! WP         [2019/07/05] -wp-prover <p> now defaults to <why3:p> (including default alt-ergo)
+- WP          [2019/09/16] Deprecated & Renamed -wp-script into -wp-coq-script
+- WP          [2019/09/16] Deprecated & Renamed -wp-update-script into -wp-update-coq-script
+- WP          [2019/09/16] Deprecated & Renamed -wp-tactic into -wp-coq-tactic
+- WP          [2019/09/16] Deprecated & Renamed -wp-tryhints into -wp-coq-tryhints
+- WP          [2019/09/16] Deprecated & Renamed -wp-hints into -wp-coq-hints
+- WP          [2019/09/16] Renamed -wp-why-opt into -wp-why3-opt
+- WP          [2019/09/16] Renamed -wp-init-alias into -wp-alias-init
+- WP          [2019/09/16] Removed -wp-include
+- WP          [2019/09/16] Removed -wp-why3
+- WP          [2019/09/16] Removed -wp-why-lib
+- WP          [2019/09/16] Removed -wp-depth
+- WP          [2019/09/16] Default -wp-extensional changed to true
+- WP          [2019/09/16] Default -wp-init-const changed to true
+-! WP         [2019/07/05] Default -wp-prover <p> changed to <why3:p> (including default alt-ergo)
 -! WP         [2019/07/05] Use native Why3 API (now requires why3 at compile time)
 - WP          [2019/06/27] Improving Cint simplifier and quantifier introduction
 o Qed         [2019/06/27] More secure API for quantifier management
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index f1e5eb696a3302ef8d4da90ea9428d9d62c21219..7025d131236ad309df05999b39890dd7ce913efd 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -726,7 +726,7 @@ let smp_cmp_with_lsr cmp a0 b0 =
        e/A2 cmp b2 <==> (e/A2)*A2 cmp b2*A2) with A2==2**a2
        So, A2>0 and (e/A2)*A2 == e&~((2**a2)-1)
     *)
-    mk_cmp_with_lsr_cst e_eq e a2 b1
+    mk_cmp_with_lsr_cst cmp e a2 b1
   with Not_found ->
     (* This rule takes into acount several cases.
        One of them is
diff --git a/src/plugins/wp/Conditions.mli b/src/plugins/wp/Conditions.mli
index 583d3289c0a2e73140884f09cb795ecc8d01394e..8f109852696f530dd785c9876ae28e309da228f4 100644
--- a/src/plugins/wp/Conditions.mli
+++ b/src/plugins/wp/Conditions.mli
@@ -134,6 +134,7 @@ val subst : (term -> term) -> sequent -> sequent
     Function [f] should only transform the head of the predicate, and can assume
     its sub-terms have been already substituted. The atomic substitution is also applied
     to predicates.
+    [f] should raise [Not_found] on terms that must not be replaced
 *)
 
 val introduction : sequent -> sequent option
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index e88783bd3830cc6ae6295d6a397b186c69b72fd3..88258560f1f600fb7a8abddf69aae8a6ba3b2e02 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -27,6 +27,10 @@ type state =
   | Composer of ProofEngine.tree * GuiTactic.composer * GuiSequent.target
   | Browser of ProofEngine.tree * GuiTactic.browser * GuiSequent.target
 
+let on_proof_context proof job data =
+  let ctxt = ProofEngine.tree_context proof in
+  WpContext.on_context ctxt job data
+
 (* -------------------------------------------------------------------------- *)
 (* --- Autofocus Management                                               --- *)
 (* -------------------------------------------------------------------------- *)
@@ -383,19 +387,21 @@ class pane (gprovers : GuiConfig.provers) =
           strategies#connect None ;
           List.iter (fun tactic -> tactic#clear) tactics
       | Some(tree,sequent,sel) ->
-          strategies#connect (Some (self#strategies sequent)) ;
-          let select (tactic : GuiTactic.tactic) =
-            let process = self#apply in
-            let composer = self#compose in
-            let browser = self#browse in
-            tactic#select ~process ~composer ~browser ~tree sel
-          in
-          let ctxt = ProofEngine.tree_context tree in
-          WpContext.on_context ctxt (List.iter select) tactics ;
-          let tgt =
-            if List.exists (fun tactics -> tactics#targeted) tactics
-            then sel else Tactical.Empty in
-          printer#set_target tgt
+          on_proof_context tree
+            begin fun () ->
+              strategies#connect (Some (self#strategies sequent)) ;
+              let select (tactic : GuiTactic.tactic) =
+                let process = self#apply in
+                let composer = self#compose in
+                let browser = self#browse in
+                tactic#select ~process ~composer ~browser ~tree sel
+              in
+              List.iter select tactics ;
+              let tgt =
+                if List.exists (fun tactics -> tactics#targeted) tactics
+                then sel else Tactical.Empty in
+              printer#set_target tgt
+            end ()
 
     method private update_scriptbar =
       match state with
@@ -519,42 +525,39 @@ class pane (gprovers : GuiConfig.provers) =
             text#hrule ;
           end
       | Proof proof ->
-          begin
-            text#clear ;
-            scripter#tree proof ;
-            text#hrule ;
-            text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;
-            text#hrule ;
-            scripter#status proof ;
-          end
+          on_proof_context proof
+            begin fun () ->
+              text#clear ;
+              scripter#tree proof ;
+              text#hrule ;
+              text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;
+              text#hrule ;
+              scripter#status proof ;
+            end ()
       | Composer(proof,cc,tgt) ->
-          begin
-            text#clear ;
-            let quit () =
-              state <- Proof proof ;
-              printer#restore tgt ;
-              self#update in
-            let ctxt = ProofEngine.tree_context proof in
-            let print = composer#print cc ~quit in
-            text#printf "%t@." (WpContext.on_context ctxt print) ;
-            text#hrule ;
-            text#printf "%t@."
-              (printer#goal (ProofEngine.head proof)) ;
-          end
+          on_proof_context proof
+            begin fun () ->
+              text#clear ;
+              let quit () =
+                state <- Proof proof ;
+                printer#restore tgt ;
+                self#update in
+              text#printf "%t@." (composer#print cc ~quit) ;
+              text#hrule ;
+              text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;
+            end ()
       | Browser(proof,cc,tgt) ->
-          begin
-            text#clear ;
-            let quit () =
-              state <- Proof proof ;
-              printer#restore tgt ;
-              self#update in
-            let ctxt = ProofEngine.tree_context proof in
-            let print = browser#print cc ~quit in
-            text#printf "%t@." (WpContext.on_context ctxt print) ;
-            text#hrule ;
-            text#printf "%t@."
-              (printer#goal (ProofEngine.head proof)) ;
-          end
+          on_proof_context proof
+            begin fun () ->
+              text#clear ;
+              let quit () =
+                state <- Proof proof ;
+                printer#restore tgt ;
+                self#update in
+              text#printf "%t@." (browser#print cc ~quit) ;
+              text#hrule ;
+              text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;
+            end ()
       | Forking _ -> ()
 
     method update =
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 30bd663bb6d935ecc6b42ab11ad07cf18bf0def0..295acb36142011bdd3c2092804ae9ec7934b61d0 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -914,9 +914,8 @@ class visitor (ctx:context) c =
                 let t = share cnv Prop (Lang.F.e_prop p) in
                 let t =
                   Why3.Term.t_forall_close vars []
-                    (Why3.Term.t_equ
-                       (Why3.Term.t_app id (List.map Why3.Term.t_var vars) result)
-                       t)
+                    (Why3.Term.t_iff t
+                       (Why3.Term.t_app id (List.map Why3.Term.t_var vars) result))
                 in
                 let decl =
                   Why3.Decl.create_prop_decl Why3.Decl.Paxiom
@@ -934,8 +933,16 @@ class visitor (ctx:context) c =
                 let decl = Why3.Decl.create_logic_decl [decl] in
                 ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl
           end
-        | Inductive _dl ->
-            why3_failure "inductive definitions not yet implemented"
+        | Inductive dl ->
+            (* create predicate symbol *)
+            let id = Why3.Ident.id_fresh (Qed.Export.link_name (lfun_name d.d_lfun)) in
+            let map e = Why3.Opt.get (of_tau ~cnv (Lang.F.tau_of_var e)) in
+            let ty_args = List.map map d.d_params in
+            let id = Why3.Term.create_lsymbol id ty_args None in
+            let decl = Why3.Decl.create_param_decl id in
+            ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl ;
+            (* register axioms *)
+            List.iter (self#on_dlemma) dl
       end
 
   end
diff --git a/src/plugins/wp/TacOverflow.ml b/src/plugins/wp/TacOverflow.ml
index 381d65d4b6c19362fd87c6d9543e78724cacde37..1585f91ab78a7b821baa21c4ac1932603119a708 100644
--- a/src/plugins/wp/TacOverflow.ml
+++ b/src/plugins/wp/TacOverflow.ml
@@ -48,7 +48,7 @@ class overflow =
                 "In-Range", (hs , cond) ;
                 "No-Overflow" ,
                 Conditions.subst
-                  (fun u -> if u == e then v else u)
+                  (fun u -> if u == e then v else raise Not_found)
                   (hs , F.p_imply cond g)
               ])
       | _ -> Not_applicable
diff --git a/src/plugins/wp/Tactical.ml b/src/plugins/wp/Tactical.ml
index 8bfb88d4f40c115f861e642236f18c71dec6a6c4..f61c15b6cb05d322f453a262ffa999e2224c347a 100644
--- a/src/plugins/wp/Tactical.ml
+++ b/src/plugins/wp/Tactical.ml
@@ -366,7 +366,7 @@ let rewrite ?at patterns sequent =
     (fun (descr,guard,src,tgt) ->
        let sequent =
          Conditions.subst
-           (fun e -> if e == src then tgt else e)
+           (fun e -> if e == src then tgt else raise Not_found)
            sequent in
        let step = Conditions.(step ~descr (When guard)) in
        descr , Conditions.insert ?at step sequent
diff --git a/src/plugins/wp/tests/wp_acsl/inductive.i b/src/plugins/wp/tests/wp_acsl/inductive.i
new file mode 100644
index 0000000000000000000000000000000000000000..5f3e2839f7510e61334ea67efb2550442f5a5b64
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/inductive.i
@@ -0,0 +1,68 @@
+/* run.config
+   OPT:-wp-prover=why3 -wp-gen -wp-msg-key print-generated
+*/
+/* run.config_qualif
+   DONTRUN:
+*/
+
+/*@ inductive is_gcd(integer a, integer b, integer d) {
+    case gcd_zero:
+      \forall integer n; is_gcd(n, 0, n);
+    case gcd_succ:
+      \forall integer a, b, d;
+      is_gcd(b, a % b, d) ==> is_gcd(a, b, d);
+    }
+*/
+
+/*@ lemma test_no_label:
+  \forall integer a, b, d ;
+  is_gcd(a, b, d) ==> is_gcd(b, d, a) ==> \false ;
+*/
+
+typedef struct _list { int element; struct _list* next; } list;
+
+/*@ inductive reachable{L} (list* root, list* node) {
+    case root_reachable{L}:
+         \forall list* root; reachable(root,root);
+    case next_reachable{L}:
+         \forall list* root, *node;
+         \valid(root) ==> reachable(root->next, node) ==> reachable(root,node);
+  }
+*/
+
+/*@ lemma test_one_label{L1, L2}:
+  \forall list *l1, *l2 ;
+  reachable{L1}(l1, l2) ==> reachable{L2}(l1, l2) ==> \false ;
+*/
+
+/*@ predicate swap{L1, L2}(int *a, int *b, integer begin, integer i, integer j, integer end) =
+       begin <= i < j < end &&
+       \at(a[i], L1) == \at(b[j], L2) &&
+       \at(a[j], L1) == \at(b[i], L2) &&
+       \forall integer k; begin <= k < end && k != i && k != j ==>
+       \at(a[k], L1) == \at(b[k], L2);
+
+    predicate same_array{L1,L2}(int *a, int *b, integer begin, integer end) =
+      \forall integer k; begin <= k < end ==> \at(a[k],L1) == \at(b[k],L2);
+
+    inductive same_elements{L1, L2}(int *a, int *b, integer begin, integer end) {
+      case refl{L1, L2}:
+        \forall int *a, int *b, integer begin, end;
+        same_array{L1,L2}(a, b, begin, end) ==>
+        same_elements{L1, L2}(a, b, begin, end);
+      case swap{L1, L2}: \forall int *a, int *b, integer begin, i, j, end;
+        swap{L1, L2}(a, b, begin, i, j, end) ==>
+        same_elements{L1, L2}(a, b, begin, end);
+      case trans{L1, L2, L3}: \forall int* a, int *b, int *c, integer begin, end;
+        same_elements{L1, L2}(a, b, begin, end) ==>
+        same_elements{L2, L3}(b, c, begin, end) ==>
+        same_elements{L1, L3}(a, c, begin, end);
+    }
+*/
+
+/*@ lemma test_multilabel{L1, L2, L3}:
+  \forall int *a, *b, integer b1, b2, e1, e2 ;
+  same_elements{L1, L2}(a, b, b1, e1) ==>
+  same_elements{L2, L3}(b, a, b2, e2) ==>
+    \false ;
+*/
\ No newline at end of file
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d8cb3e9a8d05e830be50775f2197d99d3aaa12af
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
@@ -0,0 +1,193 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/inductive.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] 3 goals scheduled
+[wp:print-generated] 
+  theory WP
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    predicate P_is_gcd int int int
+    
+    axiom Q_gcd_zero : forall n:int. P_is_gcd n 0 n
+    
+    axiom Q_gcd_succ :
+      forall a:int, b:int, d:int. P_is_gcd b (mod a b) d -> P_is_gcd a b d
+    
+    lemma Q_test_no_label :
+      forall a:int, b:int, d:int. P_is_gcd a b d -> not P_is_gcd b d a
+    
+    (* use frama_c_wp.memory.Memory *)
+    
+    (* use Compound *)
+    
+    predicate P_reachable (int -> int) (addr -> addr) addr addr
+    
+    axiom Q_root_reachable :
+      forall malloc:int -> int, mptr:addr -> addr, root:addr.
+       P_reachable malloc mptr root root
+    
+    axiom Q_next_reachable :
+      forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
+       valid_rw malloc root 2 ->
+       P_reachable malloc mptr (get mptr (shiftfield_F1__list_next root)) node ->
+       P_reachable malloc mptr root node
+    
+    goal wp_goal :
+      forall t:int -> int, t1:addr -> addr, t2:int -> int, t3:addr -> addr, a:
+       addr, a1:addr. P_reachable t2 t3 a a1 -> not P_reachable t t1 a a1
+  end
+[wp:print-generated] 
+  theory WP1
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    predicate P_is_gcd1 int int int
+    
+    axiom Q_gcd_zero1 : forall n:int. P_is_gcd1 n 0 n
+    
+    axiom Q_gcd_succ1 :
+      forall a:int, b:int, d:int. P_is_gcd1 b (mod a b) d -> P_is_gcd1 a b d
+    
+    goal wp_goal :
+      forall i:int, i1:int, i2:int. P_is_gcd1 i i1 i2 -> not P_is_gcd1 i1 i2 i
+  end
+[wp:print-generated] 
+  theory WP2
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use frama_c_wp.memory.Memory *)
+    
+    (* use Compound *)
+    
+    predicate P_reachable1 (int -> int) (addr -> addr) addr addr
+    
+    axiom Q_root_reachable1 :
+      forall malloc:int -> int, mptr:addr -> addr, root:addr.
+       P_reachable1 malloc mptr root root
+    
+    axiom Q_next_reachable1 :
+      forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
+       valid_rw malloc root 2 ->
+       P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root)) node ->
+       P_reachable1 malloc mptr root node
+    
+    lemma Q_test_one_label :
+      forall malloc:int -> int, mptr:addr -> addr, malloc1:int -> int, mptr1:
+       addr -> addr, l1:addr, l2:addr.
+       P_reachable1 malloc1 mptr1 l1 l2 -> not P_reachable1 malloc mptr l1 l2
+    
+    predicate P_is_gcd2 int int int
+    
+    axiom Q_gcd_zero2 : forall n:int. P_is_gcd2 n 0 n
+    
+    axiom Q_gcd_succ2 :
+      forall a:int, b:int, d:int. P_is_gcd2 b (mod a b) d -> P_is_gcd2 a b d
+    
+    lemma Q_test_no_label1 :
+      forall a:int, b:int, d:int. P_is_gcd2 a b d -> not P_is_gcd2 b d a
+    
+    predicate P_same_array (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:
+      addr) (begin:int) (end1:int) =
+      forall i:int.
+       begin <= i ->
+       i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b i)
+    
+    predicate P_swap (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:addr)
+      (begin:int) (i:int) (j:int) (end1:int) =
+      ((((get mint1 (shift_sint32 a i) = get mint (shift_sint32 b j) /\
+          get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
+         begin <= i) /\
+        i < j) /\
+       j < end1) /\
+      (forall i1:int.
+        not i1 = i ->
+        not j = i1 ->
+        begin <= i1 ->
+        i1 < end1 ->
+        get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
+    
+    predicate P_same_elements (addr -> int) (addr -> int) addr addr int int
+    
+    axiom Q_refl :
+      forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:int,
+       end1:int.
+       P_same_array mint mint1 a b begin end1 ->
+       P_same_elements mint mint1 a b begin end1
+    
+    axiom Q_swap :
+      forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:int, i:
+       int, j:int, end1:int.
+       P_swap mint mint1 a b begin i j end1 ->
+       P_same_elements mint mint1 a b begin end1
+    
+    axiom Q_trans :
+      forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:addr, b:
+       addr, c:addr, begin:int, end1:int.
+       P_same_elements mint mint1 b c begin end1 ->
+       P_same_elements mint1 mint2 a b begin end1 ->
+       P_same_elements mint mint2 a c begin end1
+    
+    goal wp_goal :
+      forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, a1:addr, i:
+       int, i1:int, i2:int, i3:int.
+       P_same_elements t1 t2 a a1 i i2 -> not P_same_elements t t1 a1 a i1 i3
+  end
+[wp] 3 goals generated
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Lemma test_multilabel:
+Assume: 'test_one_label' 'test_no_label'
+Prove: (P_same_elements Mint_1 Mint_2 a_0 b_0 b1_0 e1_0)
+       -> (not (P_same_elements Mint_0 Mint_1 b_0 a_0 b2_0 e2_0))
+
+------------------------------------------------------------
+
+Lemma test_no_label:
+Prove: (P_is_gcd a_0 b_0 d_0) -> (not (P_is_gcd b_0 d_0 a_0))
+
+------------------------------------------------------------
+
+Lemma test_one_label:
+Assume: 'test_no_label'
+Prove: (P_reachable Malloc_1 Mptr_1 l1_0 l2_0)
+       -> (not (P_reachable Malloc_0 Mptr_0 l1_0 l2_0))
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a45be8713b32199aad2c18ada8c43ed5fb063ea1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
@@ -0,0 +1,46 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/predicates_functions.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] 1 goal scheduled
+[wp:print-generated] 
+  theory WP
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    predicate P_P (i:int) = i = 42
+    
+    predicate P_RP int
+    
+    axiom P_RP_def :
+      forall i:int. i <= 0 \/ P_P i /\ P_RP ((- 1) + i) <-> P_RP i
+    
+    function L_F (i:int) : int = 2 * i
+    
+    function L_RF int : int
+    
+    axiom L_RF_def :
+      forall i:int. L_RF i = (if i <= 0 then 0 else L_F i + L_RF ((- 1) + i))
+    
+    goal wp_goal : forall i:int. 0 < i -> P_RP (L_RF i)
+  end
+[wp] 1 goal generated
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Lemma foo:
+Prove: (0<i_0) -> (P_RP (L_RF i_0))
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/predicates_functions.i b/src/plugins/wp/tests/wp_acsl/predicates_functions.i
new file mode 100644
index 0000000000000000000000000000000000000000..d54998f4cedefdd31991f8557bb9119e683e3430
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/predicates_functions.i
@@ -0,0 +1,14 @@
+/* run.config
+   OPT:-wp-prover=why3 -wp-gen -wp-msg-key print-generated
+*/
+/* run.config_qualif
+   DONTRUN:
+*/
+
+/*@ predicate P(integer i) = i == 42 ; */
+/*@ predicate RP(integer i) = (i <= 0) || ( P(i) && RP(i-1) ) ; */
+
+/*@ logic integer F(integer i) = i * 2 ; */
+/*@ logic integer RF(integer i) = (i <= 0) ? 0 : F(i) + RF(i-1) ; */
+
+/*@ lemma foo: \forall integer i ; i > 0 ==> RP(RF(i)) ; */
\ No newline at end of file
diff --git a/tests/fc_script/oracle/GNUmakefile b/tests/fc_script/oracle/GNUmakefile
index 32e5f33f164497fed2b82f1f27117a01a2286360..c7f456e4db883cb2d9e1609c8a84a0e9767d0a2e 100644
--- a/tests/fc_script/oracle/GNUmakefile
+++ b/tests/fc_script/oracle/GNUmakefile
@@ -29,6 +29,7 @@ CPPFLAGS    +=
 
 # (Optional) Frama-C general flags (parsing and kernel)
 FCFLAGS     += \
+  -main eva_main \
   -machdep x86_64 \
   -json-compilation-database . \
   -kernel-warn-key annot:missing-spec=abort \
diff --git a/tests/journal/oracle/intra.res.oracle b/tests/journal/oracle/intra.res.oracle
index 9032dd6f7aef8be7a8e414890d3e99b037adf17d..2685f39927be4bd34322f4a498a8a0ab31ea3cb3 100644
--- a/tests/journal/oracle/intra.res.oracle
+++ b/tests/journal/oracle/intra.res.oracle
@@ -68,7 +68,7 @@
   0 alarms generated by the analysis.
   ----------------------------------------------------------------------------
   Evaluation of the logical properties reached by the analysis:
-    Assertions        6 valid     0 unknown     0 invalid      6 total
+    Assertions        4 valid     0 unknown     0 invalid      4 total
     Preconditions     0 valid     0 unknown     0 invalid      0 total
   100% of the logical properties reached have been proven.
   ----------------------------------------------------------------------------
diff --git a/tests/misc/oracle/bts1201.res.oracle b/tests/misc/oracle/bts1201.res.oracle
index b15cb77c71ad3712d598439a18afb2b5be94afb6..5d683d1decf911024bb296418d7fb0ea6661b50a 100644
--- a/tests/misc/oracle/bts1201.res.oracle
+++ b/tests/misc/oracle/bts1201.res.oracle
@@ -35,10 +35,7 @@
   ----------------------------------------------------------------------------
   0 alarms generated by the analysis.
   ----------------------------------------------------------------------------
-  Evaluation of the logical properties reached by the analysis:
-    Assertions        1 valid     0 unknown     0 invalid      1 total
-    Preconditions     0 valid     0 unknown     0 invalid      0 total
-  100% of the logical properties reached have been proven.
+  No logical properties have been reached by the analysis.
   ----------------------------------------------------------------------------
 /* Generated by Frama-C */
 void main(void)
diff --git a/tests/value/oracle/summary.0.res.oracle b/tests/value/oracle/summary.0.res.oracle
index fe68cdf367b9ebc43d0a69b2de88ec79fd1a6378..3229f4ccf36d2a7a4b4b2c647a5d7f5da54cae4c 100644
--- a/tests/value/oracle/summary.0.res.oracle
+++ b/tests/value/oracle/summary.0.res.oracle
@@ -5,14 +5,14 @@
 [eva:initial-state] Values of globals at initialization
   undet ∈ [--..--]
   volatile_d ∈ [--..--]
-[kernel:annot:missing-spec] tests/value/summary.i:18: Warning: 
+[kernel:annot:missing-spec] tests/value/summary.i:19: Warning: 
   Neither code nor specification for function minimalist, generating default assigns from the prototype
 [eva] using specification for function minimalist
 [eva] done for function minimalist
 [eva] ====== VALUES COMPUTED ======
 [eva:summary] ====== ANALYSIS SUMMARY ======
   ----------------------------------------------------------------------------
-  0 functions analyzed (out of 4): 0% coverage.
+  0 functions analyzed (out of 6): 0% coverage.
   ----------------------------------------------------------------------------
   Some errors and warnings have been raised during the analysis:
     by the Eva analyzer:      0 errors    0 warnings
diff --git a/tests/value/oracle/summary.1.res.oracle b/tests/value/oracle/summary.1.res.oracle
index c3d37ddacc8540eb714fae0b9b041752aa5a0383..22e89c6c41bc3cc3fd942cfb5ac9836f43a89723 100644
--- a/tests/value/oracle/summary.1.res.oracle
+++ b/tests/value/oracle/summary.1.res.oracle
@@ -12,7 +12,7 @@
   
 [eva:summary] ====== ANALYSIS SUMMARY ======
   ----------------------------------------------------------------------------
-  1 function analyzed (out of 4): 25% coverage.
+  1 function analyzed (out of 6): 16% coverage.
   In this function, 1 statements reached (out of 1): 100% coverage.
   ----------------------------------------------------------------------------
   No errors or warnings raised during the analysis.
diff --git a/tests/value/oracle/summary.2.res.oracle b/tests/value/oracle/summary.2.res.oracle
index 642453d63930e4727c5d6ac5f842e6f7657f2cce..eab565f4a312fca620dc19315fa9aab51302b240 100644
--- a/tests/value/oracle/summary.2.res.oracle
+++ b/tests/value/oracle/summary.2.res.oracle
@@ -5,17 +5,17 @@
 [eva:initial-state] Values of globals at initialization
   undet ∈ [--..--]
   volatile_d ∈ [--..--]
-[eva:alarm] tests/value/summary.i:14: Warning: division by zero. assert 0 ≢ 0;
+[eva:alarm] tests/value/summary.i:15: Warning: division by zero. assert 0 ≢ 0;
 [eva] Recording results for bottom
 [eva] done for function bottom
-[eva] tests/value/summary.i:14: 
+[eva] tests/value/summary.i:15: 
   assertion 'Eva,division_by_zero' got final status invalid.
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function bottom:
   NON TERMINATING FUNCTION
 [eva:summary] ====== ANALYSIS SUMMARY ======
   ----------------------------------------------------------------------------
-  1 function analyzed (out of 4): 25% coverage.
+  1 function analyzed (out of 6): 16% coverage.
   In this function, 1 statements reached (out of 2): 50% coverage.
   ----------------------------------------------------------------------------
   No errors or warnings raised during the analysis.
diff --git a/tests/value/oracle/summary.3.res.oracle b/tests/value/oracle/summary.3.res.oracle
index 800aa84f7f444f248e282ca4458e5872cd1cea8b..f5bcadc1abb5d0f1908434ef0ff16c53d5cdbe34 100644
--- a/tests/value/oracle/summary.3.res.oracle
+++ b/tests/value/oracle/summary.3.res.oracle
@@ -6,56 +6,64 @@
   undet ∈ [--..--]
   volatile_d ∈ [--..--]
 [eva] computing for function alarms <- main.
-  Called from tests/value/summary.i:52.
-[eva:alarm] tests/value/summary.i:26: Warning: 
+  Called from tests/value/summary.i:62.
+[eva:alarm] tests/value/summary.i:27: Warning: 
   out of bounds read. assert \valid_read(p);
-[eva:alarm] tests/value/summary.i:28: Warning: 
-  out of bounds write. assert \valid(p);
 [eva:alarm] tests/value/summary.i:29: Warning: 
+  out of bounds write. assert \valid(p);
+[eva:alarm] tests/value/summary.i:30: Warning: 
   accessing out of bounds index. assert 0 ≤ undet;
-[eva:alarm] tests/value/summary.i:29: Warning: 
-  accessing out of bounds index. assert undet < 10;
 [eva:alarm] tests/value/summary.i:30: Warning: 
-  division by zero. assert undet ≢ 0;
+  accessing out of bounds index. assert undet < 10;
 [eva:alarm] tests/value/summary.i:31: Warning: 
+  division by zero. assert undet ≢ 0;
+[eva:alarm] tests/value/summary.i:32: Warning: 
   signed overflow. assert -2147483648 ≤ undet + undet;
-[eva:alarm] tests/value/summary.i:31: Warning: 
-  signed overflow. assert undet + undet ≤ 2147483647;
 [eva:alarm] tests/value/summary.i:32: Warning: 
+  signed overflow. assert undet + undet ≤ 2147483647;
+[eva:alarm] tests/value/summary.i:33: Warning: 
   invalid LHS operand for left shift. assert 0 ≤ undet;
-[eva:alarm] tests/value/summary.i:32: Warning: 
+[eva:alarm] tests/value/summary.i:33: Warning: 
   invalid RHS operand for shift. assert 0 ≤ undet < 32;
-[eva:alarm] tests/value/summary.i:32: Warning: 
-  signed overflow. assert undet << undet ≤ 2147483647;
 [eva:alarm] tests/value/summary.i:33: Warning: 
-  non-finite double value. assert \is_finite(volatile_d);
+  signed overflow. assert undet << undet ≤ 2147483647;
 [eva:alarm] tests/value/summary.i:34: Warning: 
-  non-finite double value. assert \is_finite((double)(d - d));
+  non-finite double value. assert \is_finite(volatile_d);
 [eva:alarm] tests/value/summary.i:35: Warning: 
+  non-finite double value. assert \is_finite((double)(d - d));
+[eva:alarm] tests/value/summary.i:36: Warning: 
   overflow in conversion from floating-point to integer.
   assert -2147483649 < d;
-[eva:alarm] tests/value/summary.i:35: Warning: 
+[eva:alarm] tests/value/summary.i:36: Warning: 
   overflow in conversion from floating-point to integer. assert d < 2147483648;
-[eva:alarm] tests/value/summary.i:38: Warning: 
-  pointer subtraction. assert \base_addr(p) ≡ \base_addr(q);
 [eva:alarm] tests/value/summary.i:39: Warning: 
+  pointer subtraction. assert \base_addr(p) ≡ \base_addr(q);
+[eva:alarm] tests/value/summary.i:40: Warning: 
   pointer comparison. assert \pointer_comparable((void *)p, (void *)q);
-[eva:locals-escaping] tests/value/summary.i:42: Warning: 
+[eva:locals-escaping] tests/value/summary.i:43: Warning: 
   locals {z} escaping the scope of a block of alarms through p
-[eva:alarm] tests/value/summary.i:44: Warning: 
+[eva:alarm] tests/value/summary.i:45: Warning: 
   accessing left-value that contains escaping addresses.
   assert ¬\dangling(&p);
 [eva] Recording results for alarms
 [eva] Done for function alarms
+[eva] computing for function logic <- main.
+  Called from tests/value/summary.i:63.
+[eva] tests/value/summary.i:53: assertion got status valid.
+[eva:alarm] tests/value/summary.i:54: Warning: assertion got status unknown.
+[eva:alarm] tests/value/summary.i:56: Warning: 
+  assertion got status invalid (stopping propagation).
+[eva] Recording results for logic
+[eva] Done for function logic
 [eva] computing for function f <- main.
-  Called from tests/value/summary.i:53.
-[kernel:annot:missing-spec] tests/value/summary.i:53: Warning: 
+  Called from tests/value/summary.i:64.
+[kernel:annot:missing-spec] tests/value/summary.i:64: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
 [eva] using specification for function f
 [eva] Done for function f
 [eva] computing for function g <- main.
-  Called from tests/value/summary.i:54.
-[kernel:annot:missing-spec] tests/value/summary.i:54: Warning: 
+  Called from tests/value/summary.i:65.
+[kernel:annot:missing-spec] tests/value/summary.i:65: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
 [eva] using specification for function g
 [eva] Done for function g
@@ -69,12 +77,14 @@
   q ∈ {{ &x ; &y }}
   t[0..9] ∈ {0}
   d ∈ [-2147483649. .. 2147483648.]
+[eva:final-states] Values at end of function logic:
+  
 [eva:final-states] Values at end of function main:
   
 [eva:summary] ====== ANALYSIS SUMMARY ======
   ----------------------------------------------------------------------------
-  2 functions analyzed (out of 4): 50% coverage.
-  In these functions, 32 statements reached (out of 32): 100% coverage.
+  3 functions analyzed (out of 6): 50% coverage.
+  In these functions, 38 statements reached (out of 38): 100% coverage.
   ----------------------------------------------------------------------------
   Some errors and warnings have been raised during the analysis:
     by the Eva analyzer:      0 errors    1 warning
@@ -91,10 +101,15 @@
        2 illegal conversions from floating-point to integer
        2 others
   ----------------------------------------------------------------------------
-  No logical properties have been reached by the analysis.
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        1 valid     1 unknown     1 invalid      3 total
+    Preconditions     0 valid     0 unknown     0 invalid      0 total
+  33% of the logical properties reached have been proven.
   ----------------------------------------------------------------------------
 [from] Computing for function alarms
 [from] Done for function alarms
+[from] Computing for function logic
+[from] Done for function logic
 [from] Computing for function main
 [from] Computing for function f <-main
 [from] Done for function f
@@ -109,6 +124,8 @@
   NO EFFECTS
 [from] Function g:
   NO EFFECTS
+[from] Function logic:
+  NO EFFECTS
 [from] Function main:
   NO EFFECTS
 [from] ====== END OF DEPENDENCIES ======
@@ -116,6 +133,10 @@
     x; y; p; q; t[0..9]; d
 [inout] Inputs for function alarms:
     undet; volatile_d
+[inout] Out (internal) for function logic:
+    \nothing
+[inout] Inputs for function logic:
+    undet
 [inout] Out (internal) for function main:
     \nothing
 [inout] Inputs for function main:
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..80d3ffdb4b19723e3faea13031852ffe5fbcb15e
--- /dev/null
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -0,0 +1,164 @@
+[kernel] Parsing tests/value/summary.i (no preprocessing)
+[rte] annotating function alarms
+[rte] annotating function bottom
+[rte] tests/value/summary.i:15: Warning: 
+  guaranteed RTE: assert division_by_zero: 0 ≢ 0;
+[rte] annotating function dead
+[rte] annotating function logic
+[rte] annotating function main
+[rte] annotating function minimal
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  undet ∈ [--..--]
+  volatile_d ∈ [--..--]
+[eva] computing for function alarms <- main.
+  Called from tests/value/summary.i:62.
+[eva:alarm] tests/value/summary.i:27: Warning: 
+  assertion 'rte,mem_access' got status unknown.
+[eva:alarm] tests/value/summary.i:29: Warning: 
+  assertion 'rte,mem_access' got status unknown.
+[eva:alarm] tests/value/summary.i:30: Warning: 
+  assertion 'rte,index_bound' got status unknown.
+[eva:alarm] tests/value/summary.i:30: Warning: 
+  accessing out of bounds index. assert 0 ≤ undet;
+[eva:alarm] tests/value/summary.i:30: Warning: 
+  accessing out of bounds index. assert undet < 10;
+[eva:alarm] tests/value/summary.i:31: Warning: 
+  assertion 'rte,division_by_zero' got status unknown.
+[eva:alarm] tests/value/summary.i:31: Warning: 
+  division by zero. assert undet ≢ 0;
+[eva:alarm] tests/value/summary.i:32: Warning: 
+  assertion 'rte,signed_overflow' got status unknown.
+[eva:alarm] tests/value/summary.i:32: Warning: 
+  signed overflow. assert -2147483648 ≤ undet + undet;
+[eva:alarm] tests/value/summary.i:32: Warning: 
+  signed overflow. assert undet + undet ≤ 2147483647;
+[eva:alarm] tests/value/summary.i:33: Warning: 
+  assertion 'rte,shift' got status unknown.
+[eva:alarm] tests/value/summary.i:33: Warning: 
+  assertion 'rte,shift' got status unknown.
+[eva:alarm] tests/value/summary.i:33: Warning: 
+  assertion 'rte,signed_overflow' got status unknown.
+[eva:alarm] tests/value/summary.i:33: Warning: 
+  invalid LHS operand for left shift. assert 0 ≤ undet;
+[eva:alarm] tests/value/summary.i:33: Warning: 
+  invalid RHS operand for shift. assert 0 ≤ undet < 32;
+[eva:alarm] tests/value/summary.i:33: Warning: 
+  signed overflow. assert undet << undet ≤ 2147483647;
+[eva:alarm] tests/value/summary.i:34: Warning: 
+  non-finite double value. assert \is_finite(volatile_d);
+[eva:alarm] tests/value/summary.i:35: Warning: 
+  assertion 'rte,is_nan_or_infinite' got status unknown.
+[eva:alarm] tests/value/summary.i:35: Warning: 
+  non-finite double value. assert \is_finite((double)(d - d));
+[eva:alarm] tests/value/summary.i:36: Warning: 
+  assertion 'rte,float_to_int' got status unknown.
+[eva:alarm] tests/value/summary.i:39: Warning: 
+  pointer subtraction. assert \base_addr(p) ≡ \base_addr(q);
+[eva:alarm] tests/value/summary.i:40: Warning: 
+  pointer comparison. assert \pointer_comparable((void *)p, (void *)q);
+[eva:locals-escaping] tests/value/summary.i:43: Warning: 
+  locals {z} escaping the scope of a block of alarms through p
+[eva:alarm] tests/value/summary.i:45: Warning: 
+  assertion 'rte,mem_access' got status unknown.
+[eva:alarm] tests/value/summary.i:45: Warning: 
+  accessing left-value that contains escaping addresses.
+  assert ¬\dangling(&p);
+[eva] Recording results for alarms
+[eva] Done for function alarms
+[eva] computing for function logic <- main.
+  Called from tests/value/summary.i:63.
+[eva] tests/value/summary.i:53: assertion got status valid.
+[eva:alarm] tests/value/summary.i:54: Warning: assertion got status unknown.
+[eva:alarm] tests/value/summary.i:56: Warning: 
+  assertion got status invalid (stopping propagation).
+[eva] Recording results for logic
+[eva] Done for function logic
+[eva] computing for function f <- main.
+  Called from tests/value/summary.i:64.
+[kernel:annot:missing-spec] tests/value/summary.i:64: Warning: 
+  Neither code nor specification for function f, generating default assigns from the prototype
+[eva] using specification for function f
+[eva] Done for function f
+[eva] computing for function g <- main.
+  Called from tests/value/summary.i:65.
+[kernel:annot:missing-spec] tests/value/summary.i:65: Warning: 
+  Neither code nor specification for function g, generating default assigns from the prototype
+[eva] using specification for function g
+[eva] Done for function g
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function alarms:
+  x ∈ [--..--]
+  y ∈ {0}
+  p ∈ {{ &x ; &y }}
+  q ∈ {{ &x ; &y }}
+  t[0..9] ∈ {0}
+  d ∈ [-2147483649. .. 2147483648.]
+[eva:final-states] Values at end of function logic:
+  
+[eva:final-states] Values at end of function main:
+  
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  3 functions analyzed (out of 6): 50% coverage.
+  In these functions, 38 statements reached (out of 38): 100% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    1 warning
+    by the Frama-C kernel:    0 errors    2 warnings
+  ----------------------------------------------------------------------------
+  18 alarms generated by the analysis:
+       1 division by zero
+       3 invalid memory accesses
+       2 accesses out of bounds index
+       3 integer overflows
+       2 invalid shifts
+       1 escaping address
+       2 nan or infinite floating-point values
+       2 illegal conversions from floating-point to integer
+       2 others
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        1 valid     1 unknown     1 invalid      3 total
+    Preconditions     0 valid     0 unknown     0 invalid      0 total
+  33% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
+[from] Computing for function alarms
+[from] Done for function alarms
+[from] Computing for function logic
+[from] Done for function logic
+[from] Computing for function main
+[from] Computing for function f <-main
+[from] Done for function f
+[from] Computing for function g <-main
+[from] Done for function g
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function alarms:
+  NO EFFECTS
+[from] Function f:
+  NO EFFECTS
+[from] Function g:
+  NO EFFECTS
+[from] Function logic:
+  NO EFFECTS
+[from] Function main:
+  NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function alarms:
+    x; y; p; q; t[0..9]; d
+[inout] Inputs for function alarms:
+    undet; volatile_d
+[inout] Out (internal) for function logic:
+    \nothing
+[inout] Inputs for function logic:
+    undet
+[inout] Out (internal) for function main:
+    \nothing
+[inout] Inputs for function main:
+    undet; volatile_d
diff --git a/tests/value/summary.i b/tests/value/summary.i
index b037fa17050b083cf6758ef68c9579ea5223544e..d73b4b42d73532f315dedb80d1c927415566d9eb 100644
--- a/tests/value/summary.i
+++ b/tests/value/summary.i
@@ -3,6 +3,7 @@
   STDOPT: +"-eva-msg-key=summary -main minimal"
   STDOPT: +"-eva-msg-key=summary -main bottom"
   STDOPT: +"-eva-msg-key=summary -main main"
+  STDOPT: +"-rte -eva-msg-key=summary -main main"
 */
 
 /* Tests the summary on the smallest possible program. */
@@ -47,9 +48,25 @@ void alarms () {
 void f(void);
 void g(void);
 
+/* 1 valid assertion, 1 unknown assertion, 1 invalid assertion. */
+void logic () {
+  /*@ assert \true; */
+  /*@ assert undet == 0; */
+  if (undet)
+    /*@ assert \false; */
+    ;
+}
+
 // 2 kernel warnings, 1 eva warning, no error.
 void main () {
   alarms ();
+  logic ();
   f(); // kernel warning: no specification for function f
   g(); // kernel warning: no specification for function g
 }
+
+/* Assertions in this function should not appear in the summary. */
+void dead () {
+  /*@ assert \true; */
+  /*@ assert \false; */
+}