diff --git a/src/plugins/value/utils/value_results.ml b/src/plugins/value/utils/value_results.ml
index 8cc88aceefd9a87fbfa0bcac72f3807755a8fe04..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
@@ -510,9 +511,9 @@ let make_report () =
| 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/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)