diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml index 9f7ddc3f46156c55e8a3159cd15db1058b988464..548a3cc8b12f85336c171ae26bb9230950b21623 100644 --- a/src/plugins/value/utils/value_util.ml +++ b/src/plugins/value/utils/value_util.ml @@ -111,17 +111,19 @@ let protect_only_once = ref true let protect f ~cleanup = let catch () = !protect_only_once && not (Kernel.SaveState.is_empty ()) in + let cleanup () = + Value_parameters.feedback ~once:true "Clean up and save partial results."; + try cleanup () + with e -> + protect_only_once := false; + raise e + in try f (); with | Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _ | Sys.Break as e when catch () -> - try - Value_parameters.feedback ~once:true "Clean up and save partial results."; - cleanup (); - raise e; - with e -> - protect_only_once := false; - raise e + cleanup (); + raise e let register_new_var v typ = if Cil.isFunctionType typ then