diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index 46b66659663dfa6bd9a47a4ba6ed6efca7c615c4..7785ba74e929f63514f7de1f5e8020f1b6c14563 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -158,14 +158,14 @@ let save_binary error_extension =
 let () =
   (* implement a refinement of the behavior described in BTS #1388:
      - on normal exit: save
-     - on Sys.break, system error or feature request: do not save
+     - on Sys.break (Ctrl-C interruption): save, but add ".break" suffix
      - on user error: save, but add ".error" suffix
      - on fatal error or unexpected error: save, but add ".crash" suffix *)
   Cmdline.at_normal_exit (fun () -> save_binary None);
   Cmdline.at_error_exit
     (function
-      | Sys.Break | Sys_error _ | Log.FeatureRequest _ -> ()
-      | Log.AbortError _ -> save_binary (Some ".error")
+      | Sys.Break -> save_binary (Some ".break")
+      | Log.AbortError _ | Log.FeatureRequest _ -> save_binary (Some ".error")
       | _ -> save_binary (Some ".crash"))
 
 (* Write JSON files to disk if required *)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 64bc3512a2b8c077dfd7a522fc00790edcf1c64c..b63abe98dc97998803b7e77f354a53aebedc043d 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -715,8 +715,6 @@ module Value = struct
          returning void (the case when the kf corresponds to a declaration *)
       raise Void_Function
 
-  exception Aborted
-
   let display = mk_fun "Value.display"
 
   let emitter = ref Emitter.dummy
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 168250349bbe570b9e89a48b79d3e39f75dbc131..ba5d56d1bd184252fcc2bfd31ecaef5405b1d98c 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -126,8 +126,6 @@ module Value : sig
   type t = Cvalue.V.t
   (** Internal representation of a value. *)
 
-  exception Aborted
-
   val emitter: Emitter.t ref
   (** Emitter used by Value to emit statuses *)
 
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index c2db72bb383b623cb8a8ddbe46313ce49a322703..276b87beebb4c1f5ef2a8607fbbfdb349b198571 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -423,10 +423,7 @@ let emit_alarms kinstr map =
   let sorted_list = List.sort cmp list in
   List.iter (fun (alarm, status) -> emit_alarm kinstr alarm status) sorted_list;
   if Alarm_cache.length () >= Value_parameters.StopAtNthAlarm.get ()
-  then begin
-    Value_parameters.log "Stopping at nth alarm" ;
-    raise Db.Value.Aborted
-  end
+  then Value_parameters.abort "Stopping at nth alarm"
 
 let emit kinstr = function
   | Just map -> if not (M.is_empty map) then emit_alarms kinstr map
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index 0aa7507ffd1a8c58911dbfd3200e7fef3072b03e..6dc0b78d39ac562b844c825419398cb11db4e7b5 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -275,15 +275,12 @@ let apply_builtin (builtin:builtin) call ~pre ~post =
     process_result call post call_result
   with
   | Invalid_nb_of_args n ->
-    Value_parameters.error ~current:true
+    Value_parameters.abort ~current:true
       "Invalid number of arguments for builtin %a: %d expected, %d found"
-      Kernel_function.pretty call.kf n (List.length arguments);
-    raise Db.Value.Aborted
+      Kernel_function.pretty call.kf n (List.length arguments)
   | Outside_builtin_possibilities ->
-    Value_parameters.warning ~once:true ~current:true
-      "Call to builtin %a failed, aborting." Kernel_function.pretty call.kf;
-    raise Db.Value.Aborted
-
+    Value_parameters.fatal ~current:true
+      "Call to builtin %a failed" Kernel_function.pretty call.kf
 
 (*
 Local Variables:
diff --git a/src/plugins/value/domains/cvalue/builtins_memory.ml b/src/plugins/value/domains/cvalue/builtins_memory.ml
index dbf489fe336a4c8ed1d72df24c37924b379ac589..c1b59f768dfa5a9877f07e581ae1997ca39670cb 100644
--- a/src/plugins/value/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/value/domains/cvalue/builtins_memory.ml
@@ -627,10 +627,9 @@ let frama_c_interval_split _state actuals =
       with
       | Cvalue.V.Not_based_on_null
       | Ival.Not_Singleton_Int ->
-        Value_parameters.error
+        Value_parameters.abort
           "Invalid call to Frama_C_interval_split%a"
-          Value_util.pretty_actuals actuals;
-        raise Db.Value.Aborted
+          Value_util.pretty_actuals actuals
     end
   | _ -> raise (Builtins.Invalid_nb_of_args 2)
 
diff --git a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
index be8049588a16c235f5a451f8e8237572ace8ab4c..9b74eeb416fd416cf0dd14aae0fea58150fb4d0c 100644
--- a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
+++ b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
@@ -123,7 +123,8 @@ let watch_hook (stmt, _callstack, states) =
            then ()
            else
              let current = Integer.pred current in
-             if Integer.is_zero current then raise Db.Value.Aborted;
+             if Integer.is_zero current then
+               Value_parameters.abort "Watchpoint builtin: countdown to zero";
              w.remaining_count <- current;
              w.stmts <- Cil_datatype.Stmt.Set.add stmt set;
          end)
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
index 26518aa8d7c76a6a249d3c082b9131c453b4bbda..59adfa1136bf985c422ea254a7eacaf2c33c9e01 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
@@ -101,10 +101,9 @@ let write_abstract_value state (lval, loc, typ) assigned_value =
     Value_parameters.result
       "State before degeneration:@\n======%a@\n======="
       Cvalue.Model.pretty state;
-    Value_util.warning_once_current
+    Value_parameters.fatal ~current:true
       "writing at a completely unknown address@[%a@].@\nAborting."
-      Origin.pretty_as_reason orig;
-    raise Db.Value.Aborted
+      Origin.pretty_as_reason orig
   | _ ->
     let exact = Locations.cardinal_zero_or_one loc in
     let value =
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index daeca950f4c145e40f5a6d5ceb176b7b1cd7d6ae..a932d0eebdcf98c0dc1a21575316dd7a9cb5208b 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -113,20 +113,25 @@ let post_analysis () =
   (* Remove redundant alarms *)
   if Value_parameters.RmAssert.get () then !Db.Value.rm_asserts ()
 
-(* Register a signal handler for SIGUSR1, that will be used to abort Value *)
-let () =
-  let prev = ref (fun _ -> ()) in
-  let handler (_signal: int) =
-    !prev Sys.sigusr1; (* Call previous signal handler *)
-    Value_parameters.warning "Stopping analysis at user request@.";
-    Iterator.signal_abort ()
+(* Registers signal handlers for SIGUSR1 and SIGINT to cleanly abort the Eva
+   analysis. Returns a function that restores previous signal behaviors after
+   the analysis. *)
+let register_signal_handler () =
+  let warn () =
+    Value_parameters.warning ~once:true "Stopping analysis at user request@."
   in
-  try
-    match Sys.signal Sys.sigusr1 (Sys.Signal_handle handler) with
-    | Sys.Signal_default | Sys.Signal_ignore -> ()
-    | Sys.Signal_handle f -> prev := f
-  with Invalid_argument _ -> () (* Ignore: SIGURSR1 is not available on Windows,
-                                   and possibly on other platforms. *)
+  let stop _ = warn (); Iterator.signal_abort () in
+  let interrupt _ = warn (); raise Sys.Break in
+  let register_handler signal handler =
+    match Sys.signal signal (Sys.Signal_handle handler) with
+    | previous_behavior -> fun () -> Sys.set_signal signal previous_behavior
+    | exception Invalid_argument _ -> fun () -> ()
+    (* Ignore: SIGURSR1 is not available on Windows,
+       and possibly on other platforms. *)
+  in
+  let restore_sigusr1 = register_handler Sys.sigusr1 stop in
+  let restore_sigint = register_handler Sys.sigint interrupt in
+  fun () -> restore_sigusr1 (); restore_sigint ()
 
 module Make (Abstract: Abstractions.Eva) = struct
 
@@ -327,7 +332,8 @@ module Make (Abstract: Abstractions.Eva) = struct
     Db.Value.Call_Value_Callbacks.apply (cvalue_state, [kf, Kglobal])
 
   let compute kf init_state =
-    try
+    let restore_signals = register_signal_handler () in
+    let compute () =
       Value_util.push_call_stack kf Kglobal;
       store_initial_state kf init_state;
       let call =
@@ -344,16 +350,13 @@ module Make (Abstract: Abstractions.Eva) = struct
       post_analysis ();
       Abstract.Dom.post_analysis final_state;
       Value_results.print_summary ();
-    with
-    | Db.Value.Aborted ->
+      restore_signals ()
+    in
+    let cleanup () =
       Abstract.Dom.Store.mark_as_computed ();
-      post_analysis_cleanup ~aborted:true;
-      (* Signal that a degeneration occurred *)
-      if Value_util.DegenerationPoints.length () > 0 then
-        Value_parameters.error
-          "Degeneration occurred:@\nresults are not correct for lines of code \
-           that can be reached from the degeneration point.@."
-
+      post_analysis_cleanup ~aborted:true
+    in
+    Value_util.protect compute ~cleanup
 
   let compute_from_entry_point kf ~lib_entry =
     pre_analysis ();
@@ -361,10 +364,9 @@ module Make (Abstract: Abstractions.Eva) = struct
       (if lib_entry then "n in" else " ")
       Kernel_function.pretty kf;
     let initial_state =
-      try Init.initial_state_with_formals ~lib_entry kf
-      with Db.Value.Aborted ->
-        post_analysis_cleanup ~aborted:true;
-        Value_parameters.abort "Degeneration occurred during initialization, aborting."
+      Value_util.protect
+        (fun () -> Init.initial_state_with_formals ~lib_entry kf)
+        ~cleanup:(fun () -> post_analysis_cleanup ~aborted:true)
     in
     match initial_state with
     | `Bottom ->
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 30680db8febe393703da2ba94fb8893bc40beccd..933035419a65831bb45ff24fc2c41ae84fd27181 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -29,7 +29,7 @@ let check_signals, signal_abort =
   (fun () ->
      if !signal_emitted then begin
        signal_emitted := false;
-       raise Db.Value.Aborted
+       raise Sys.Break
      end),
   (fun () -> signal_emitted := true)
 
@@ -765,7 +765,7 @@ module Computer
         end)
         ()
     in
-    try
+    let compute () =
       let results = Dataflow.compute () in
       if Value_parameters.ValShowProgress.get () then
         Value_parameters.feedback "Recording results for %a"
@@ -779,11 +779,12 @@ module Computer
            Kernel_function.pretty kf;
        | _ -> ());
       results, !Dataflow.cacheable
-    with Db.Value.Aborted as e ->
-      (* analysis was aborted: pop the call stack and inform the caller *)
+    in
+    let cleanup () =
       Dataflow.mark_degeneration ();
-      Dataflow.merge_results ();
-      raise e
+      Dataflow.merge_results ()
+    in
+    Value_util.protect compute ~cleanup
 end
 
 
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 871cd1a2e967be8289afa2caf97acea54e2632a8..1ce8dd5d91ed1f126de402825f9d2298151ea620 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -315,7 +315,7 @@ module Make (Abstract: Abstractions.Eva) = struct
       (* Changed by compute_call_ref, called from process_call *)
       Cil.CurrentLoc.set (Cil_datatype.Stmt.loc stmt);
     in
-    try
+    let process () =
       let domain_valuation = Eval.to_domain_valuation valuation in
       let res =
         (* Process the call according to the domain decision. *)
@@ -328,10 +328,9 @@ module Make (Abstract: Abstractions.Eva) = struct
       in
       cleanup ();
       res
-    with Db.Value.Aborted as e ->
-      InOutCallback.clear ();
-      cleanup ();
-      raise e
+    in
+    Value_util.protect process
+      ~cleanup:(fun () -> InOutCallback.clear (); cleanup ())
 
   (* ------------------- Retro propagation on formals ----------------------- *)
 
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index 13a005dd2afb149c347bfdd8ed45f51fd90b3262..9f7ddc3f46156c55e8a3159cd15db1058b988464 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/value_util.ml
@@ -107,6 +107,22 @@ module DegenerationPoints =
       let dependencies = [ Db.Value.self ]
     end)
 
+let protect_only_once = ref true
+
+let protect f ~cleanup =
+  let catch () = !protect_only_once && not (Kernel.SaveState.is_empty ()) 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
+
 let register_new_var v typ =
   if Cil.isFunctionType typ then
     Globals.Functions.replace_by_declaration (Cil.empty_funspec()) v v.vdecl
diff --git a/src/plugins/value/utils/value_util.mli b/src/plugins/value/utils/value_util.mli
index 0bfe89cbe916816878319417b0dc123ad79bea1c..c99393d8885d66b5e1e11023582e3b7b797f05c7 100644
--- a/src/plugins/value/utils/value_util.mli
+++ b/src/plugins/value/utils/value_util.mli
@@ -51,6 +51,11 @@ val warning_once_current : ('a, Format.formatter, unit) format -> 'a
     status associated to {!Value_parameters.wkey_alarm} *)
 val alarm_report: 'a Log.pretty_printer
 
+(** [protect f ~cleanup] runs [f]. On a user interruption or a Frama-C error,
+    if option -save is set, applies [cleanup]. This is used to clean up and
+    save partial results when the analysis is aborted. *)
+val protect: (unit -> 'a) -> cleanup:(unit -> unit) -> 'a
+
 (* Statements for which the analysis has degenerated. [true] means that this is
    the statement on which the degeneration occurred, or a statement above in
    the callstack *)
diff --git a/tests/builtins/oracle/watch.res.oracle b/tests/builtins/oracle/watch.res.oracle
index 28fc5ca752290093449dfdb06b399008642ff8c5..01f0d0b2b5779644be6752cd329942be18950829 100644
--- a/tests/builtins/oracle/watch.res.oracle
+++ b/tests/builtins/oracle/watch.res.oracle
@@ -24,28 +24,5 @@
 [eva] tests/builtins/watch.c:17: Watchpoint: & c [--..--]
 [eva] tests/builtins/watch.c:18: Watchpoint: & c [--..--]
 [eva] tests/builtins/watch.c:19: Watchpoint: & c [--..--]
-[eva] User Error: Degeneration occurred:
-  results are not correct for lines of code that can be reached from the degeneration point.
-[from] Computing for function main
-[from] Computing for function Frama_C_watch_value <-main
-[from] Done for function Frama_C_watch_value
-[from] Computing for function u <-main
-[from] Done for function u
-[from] Non-terminating function main (no dependencies)
-[from] Done for function main
-[from] ====== DEPENDENCIES COMPUTED ======
-  These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_watch_value:
-  c FROM c; x_1; x_2; x_3 (and SELF)
-  \result FROM c; x_1; x_2; x_3
-[from] Function u:
-  \result FROM \nothing
-[from] Function main:
-  NON TERMINATING - NO EFFECTS
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main:
-    x; c
-[inout] Inputs for function main:
-    x
-[eva] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[eva] User Error: Watchpoint builtin: countdown to zero
 [kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/fc_script/oracle/make-wrapper.res b/tests/fc_script/oracle/make-wrapper.res
index 09358673bd043241721520d914345a9a782b35d5..8370fe5e49498ce18397bc847647adac6ce49eaf 100644
--- a/tests/fc_script/oracle/make-wrapper.res
+++ b/tests/fc_script/oracle/make-wrapper.res
@@ -25,6 +25,7 @@ Command: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-war
 [kernel:annot:missing-spec] make-wrapper.c:13: Warning: 
   Neither code nor specification for function large_name_to_force_line_break_in_stack_msg, generating default assigns from the prototype
 [kernel] User Error: warning annot:missing-spec treated as fatal error.
+[eva] Clean up and save partial results.
 [kernel] Frama-C aborted: invalid user input.
 [kernel] Warning: attempting to save on non-zero exit code: modifying filename into `PWD/make-for-make-wrapper.eva/framac.sav.error'.