diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml index 304e26b6d01015d404145a18c98d2489f1e78edb..79b128e2dfacbad5e6c453171c1a75a3eb36bd1b 100644 --- a/src/plugins/value/engine/transfer_logic.ml +++ b/src/plugins/value/engine/transfer_logic.ml @@ -629,7 +629,7 @@ module Make "valid" | Alarmset.False, `True -> change_status Property_status.False_if_reachable; - "invalid (stopping propagation)" + "invalid" ^ (if reduce then " (stopping propagation)" else "") | Alarmset.False, `Unknown -> change_status Property_status.False_if_reachable; "invalid" diff --git a/tests/value/oracle/logic.res.oracle b/tests/value/oracle/logic.res.oracle index 6a192e2ee7454a8e879e54ca332a3485eb6b6873..1920a84df5ef397cf97a49829ce57f1d79f6f942 100644 --- a/tests/value/oracle/logic.res.oracle +++ b/tests/value/oracle/logic.res.oracle @@ -253,8 +253,7 @@ [eva:alarm] tests/value/logic.c:301: Warning: assertion got status unknown. [eva:alarm] tests/value/logic.c:303: Warning: assertion got status invalid (stopping propagation). -[eva:alarm] tests/value/logic.c:306: Warning: - check got status invalid (stopping propagation). +[eva:alarm] tests/value/logic.c:306: Warning: check got status invalid. [eva] tests/value/logic.c:307: Frama_C_show_each_reachable: {42} [eva] Recording results for check_and_assert [eva] Done for function check_and_assert