diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 298ad6fe8eed25d5da9f1c0a0b0d8d56141dd2cf..64bc3512a2b8c077dfd7a522fc00790edcf1c64c 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -502,7 +502,7 @@ module Value = struct
       Callstack.Hashtbl.add by_callstack cs state
 
   let get_initial_state kf =
-    assert (is_computed ()); (* this assertion fails during value analysis *)
+    assert (is_computed ()); (* this assertion fails during Eva analysis *)
     try Called_Functions_Memo.find kf
     with Not_found ->
       let state =
@@ -517,8 +517,9 @@ module Value = struct
       Called_Functions_Memo.add kf state;
       state
 
+  (* This function is used by the Inout plugin during Eva analysis, so it
+     should not fail during Eva analysis, even if results are incomplete. *)
   let get_initial_state_callstack kf =
-    assert (is_computed ()); (* this assertion fails during value analysis *)
     try Some (Called_Functions_By_Callstack.find kf)
     with Not_found -> None
 
@@ -568,28 +569,28 @@ module Value = struct
       noassert_get_stmt_state ~after s
 
   let get_stmt_state ?(after=false) s =
-    assert (is_computed ()); (* this assertion fails during value analysis *)
+    assert (is_computed ()); (* this assertion fails during Eva analysis *)
     noassert_get_stmt_state ~after s
 
   let get_state ?(after=false) k =
-    assert (is_computed ()); (* this assertion fails during value analysis *)
+    assert (is_computed ()); (* this assertion fails during Eva analysis *)
     noassert_get_state ~after k
 
   let get_stmt_state_callstack ~after stmt =
-    assert (is_computed ()); (* this assertion fails during value analysis *)
+    assert (is_computed ()); (* this assertion fails during Eva analysis *)
     try
       Some (if after then AfterTable_By_Callstack.find stmt else
               Table_By_Callstack.find stmt)
     with Not_found -> None
 
   let fold_stmt_state_callstack f acc ~after stmt =
-    assert (is_computed ()); (* this assertion fails during value analysis *)
+    assert (is_computed ()); (* this assertion fails during Eva analysis *)
     match get_stmt_state_callstack ~after stmt with
     | None -> acc
     | Some h -> Value_types.Callstack.Hashtbl.fold (fun _ -> f) h acc
 
   let fold_state_callstack f acc ~after ki =
-    assert (is_computed ()); (* this assertion fails during value analysis *)
+    assert (is_computed ()); (* this assertion fails during Eva analysis *)
     match ki with
     | Kglobal -> f (globals_state ()) acc
     | Kstmt stmt -> fold_stmt_state_callstack f acc ~after stmt
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 4d517e199e2d2d44ea209f1a875ec0cf0d17a054..64f0a75318804c193951839e840b741787f50122 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -82,8 +82,7 @@ let pre_analysis () =
      degeneration states *)
   Value_util.DegenerationPoints.clear ();
   Cvalue.V.clear_garbled_mix ();
-  Value_util.clear_call_stack ();
-  Db.Value.mark_as_computed ()
+  Value_util.clear_call_stack ()
 
 let post_analysis_cleanup ~aborted =
   Value_util.clear_call_stack ();
@@ -341,11 +340,13 @@ module Make (Abstract: Abstractions.Eva) = struct
       let final_state = PowersetDomain.(final_states >>-: of_list >>- join) in
       Value_util.pop_call_stack ();
       Value_parameters.feedback "done for function %a" Kernel_function.pretty kf;
+      Abstract.Dom.Store.mark_as_computed ();
       post_analysis ();
       Abstract.Dom.post_analysis final_state;
       Value_results.print_summary ();
     with
     | Db.Value.Aborted ->
+      Abstract.Dom.Store.mark_as_computed ();
       post_analysis_cleanup ~aborted:true;
       (* Signal that a degeneration occurred *)
       if Value_util.DegenerationPoints.length () > 0 then
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 930c01942de58d96d47e0845553c4b4e9e249415..30680db8febe393703da2ba94fb8893bc40beccd 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -782,7 +782,6 @@ module Computer
     with Db.Value.Aborted as e ->
       (* analysis was aborted: pop the call stack and inform the caller *)
       Dataflow.mark_degeneration ();
-      Db.Value.mark_as_computed ();
       Dataflow.merge_results ();
       raise e
 end