diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml index 92bb922726edd56ff9d777164f81a30f0a6d9981..370396757e451c66c916f4c35aadec6cfede269e 100644 --- a/src/plugins/value/legacy/eval_terms.ml +++ b/src/plugins/value/legacy/eval_terms.ml @@ -1596,7 +1596,7 @@ let eval_forall_predicate state r test = let under_loc = make_loc r.eunder in forall_in_under_location state under_loc test | True -> True - | False -> False + | False -> if r.empty then Unknown else False (* Evaluation of an \initialized predicate on a location evaluated to [r] in the state [state]. *)