diff --git a/src/plugins/eva/utils/red_statuses.ml b/src/plugins/eva/utils/red_statuses.ml
index 05f4efb03c8b26180907bdf7b33d216b1610d004..b9d5032a723df3a70632725184c5485e1ff75231 100644
--- a/src/plugins/eva/utils/red_statuses.ml
+++ b/src/plugins/eva/utils/red_statuses.ml
@@ -91,17 +91,13 @@ let add_red_ap kinstr ap =
 
 let add_red_alarm ki a = add_red_ap ki (Alarm a)
 
-let add_red_property ki ip =
-  if false then
-    add_red_ap ki (Prop ip)
-  else
-    (* Collapses preconditions-at-callsites into the precondition itself,
-       by modifying the callstack. Results in a better display *)
-    let open Property in
-    match ip with
-    | IPPropertyInstance {ii_ip=IPPredicate {ip_kind=PKRequires _} as ip'} ->
-      add_red_ap Kglobal (Prop ip')
-    | _ -> add_red_ap ki (Prop ip)
+let add_red_property ki (ip: Property.identified_property) =
+  add_red_ap ki (Prop ip);
+  (* If [ip] is an instance of a precondition [ip'], also add [ip'] itself. *)
+  match ip with
+  | IPPropertyInstance {ii_ip = IPPredicate {ip_kind = PKRequires _} as ip'} ->
+    add_red_ap Kglobal (Prop ip')
+  | _ -> ()
 
 let is_red ip =
   let kinstr = Property.get_kinstr ip in
diff --git a/tests/value/oracle/red_alarms.csv b/tests/value/oracle/red_alarms.csv
index 9be0520457a4fad73c6d13ce197e9dd075deeb4e..fcbb41973efc4c55e36c4394cea6bc50f30ae775 100644
--- a/tests/value/oracle/red_alarms.csv
+++ b/tests/value/oracle/red_alarms.csv
@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
 .	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
 .	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
diff --git a/tests/value/oracle_apron/red_alarms.csv b/tests/value/oracle_apron/red_alarms.csv
index 9be0520457a4fad73c6d13ce197e9dd075deeb4e..fcbb41973efc4c55e36c4394cea6bc50f30ae775 100644
--- a/tests/value/oracle_apron/red_alarms.csv
+++ b/tests/value/oracle_apron/red_alarms.csv
@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
 .	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
 .	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
diff --git a/tests/value/oracle_bitwise/red_alarms.csv b/tests/value/oracle_bitwise/red_alarms.csv
index 9be0520457a4fad73c6d13ce197e9dd075deeb4e..fcbb41973efc4c55e36c4394cea6bc50f30ae775 100644
--- a/tests/value/oracle_bitwise/red_alarms.csv
+++ b/tests/value/oracle_bitwise/red_alarms.csv
@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
 .	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
 .	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
diff --git a/tests/value/oracle_equality/red_alarms.csv b/tests/value/oracle_equality/red_alarms.csv
index 9be0520457a4fad73c6d13ce197e9dd075deeb4e..fcbb41973efc4c55e36c4394cea6bc50f30ae775 100644
--- a/tests/value/oracle_equality/red_alarms.csv
+++ b/tests/value/oracle_equality/red_alarms.csv
@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
 .	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
 .	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
diff --git a/tests/value/oracle_gauges/red_alarms.csv b/tests/value/oracle_gauges/red_alarms.csv
index 9be0520457a4fad73c6d13ce197e9dd075deeb4e..fcbb41973efc4c55e36c4394cea6bc50f30ae775 100644
--- a/tests/value/oracle_gauges/red_alarms.csv
+++ b/tests/value/oracle_gauges/red_alarms.csv
@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
 .	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
 .	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
diff --git a/tests/value/oracle_multidim/red_alarms.csv b/tests/value/oracle_multidim/red_alarms.csv
index 9be0520457a4fad73c6d13ce197e9dd075deeb4e..fcbb41973efc4c55e36c4394cea6bc50f30ae775 100644
--- a/tests/value/oracle_multidim/red_alarms.csv
+++ b/tests/value/oracle_multidim/red_alarms.csv
@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
 .	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
 .	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
diff --git a/tests/value/oracle_octagon/red_alarms.csv b/tests/value/oracle_octagon/red_alarms.csv
index 9be0520457a4fad73c6d13ce197e9dd075deeb4e..fcbb41973efc4c55e36c4394cea6bc50f30ae775 100644
--- a/tests/value/oracle_octagon/red_alarms.csv
+++ b/tests/value/oracle_octagon/red_alarms.csv
@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
 .	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
 .	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
diff --git a/tests/value/oracle_symblocs/red_alarms.csv b/tests/value/oracle_symblocs/red_alarms.csv
index 9be0520457a4fad73c6d13ce197e9dd075deeb4e..fcbb41973efc4c55e36c4394cea6bc50f30ae775 100644
--- a/tests/value/oracle_symblocs/red_alarms.csv
+++ b/tests/value/oracle_symblocs/red_alarms.csv
@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
 .	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
 .	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
 .	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q