diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml index 2943a97ab7d3df8dae53db9a91531412dede011f..ab2f98468fb829b093a001c480cbc0803effebb4 100644 --- a/src/plugins/eva/legacy/eval_terms.ml +++ b/src/plugins/eva/legacy/eval_terms.ml @@ -2046,6 +2046,8 @@ and reduce_by_valid_string ~alarm_mode env positive ~wide ~access arg = let aux base offset acc = let value = Cvalue.V.inject base offset in let v, alarms = apply_logic_builtin wrapper env [value] in + (* Beware of not removing const strings on the negation of \valid_string. *) + let alarms = alarms || (access = Write && Base.is_read_only base) in if (positive && Cvalue.V.is_bottom v) || (not positive && not alarms) then acc