diff --git a/src/plugins/callgraph/cg.ml b/src/plugins/callgraph/cg.ml
index a5363fdb19eb75b280969f96a61ade45c75e37e2..5daf8249498f3ebf1ed13cff9c0a9929fd05e3cb 100644
--- a/src/plugins/callgraph/cg.ml
+++ b/src/plugins/callgraph/cg.ml
@@ -205,7 +205,7 @@ let syntactic_compute g =
 let semantic_compute g =
   Globals.Functions.iter
     (fun kf ->
-       let callers = !Db.Value.callers kf in
+       let callers = Eva.Results.callsites kf in
        let must_add =
          callers <> []  (* the function is called *)
          || is_entry_point kf
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 6cb042290b0944179c00f4989636aa6c80a2a469..17afc0cb0009c8dd7452ed1ee8f6940e60b21f00 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -551,13 +551,13 @@ struct
 
     (* Filter out unreachable values. *)
     let transfer_stmt s d =
-      if Db.Value.is_reachable (To_Use.get_value_state s) &&
+      if Eva.Results.is_reachable s &&
          not (Function_Froms.Memory.is_bottom d.deps_table)
       then transfer_stmt s d
       else []
 
     let doEdge s succ d =
-      if Db.Value.is_reachable (To_Use.get_value_state succ)
+      if Eva.Results.is_reachable succ
       then
         let dt = d.deps_table in
         let opened = Kernel_function.blocks_opened_by_edge s succ in
@@ -647,7 +647,7 @@ struct
           let _poped = Stack.pop call_stack in
           let last_from =
             try
-              if Db.Value.is_reachable (To_Use.get_value_state ret_id)
+              if Eva.Results.is_reachable ret_id
               then
                 externalize
                   ret_id
diff --git a/src/plugins/from/from_register.ml b/src/plugins/from/from_register.ml
index e51dcf068bc415d4295ea78d753037d8585abdbb..d807740cf802b11d785e27cf7522d8cf673567f9 100644
--- a/src/plugins/from/from_register.ml
+++ b/src/plugins/from/from_register.ml
@@ -30,7 +30,7 @@ let display fmtopt =
   Option.iter (fun fmt -> Format.fprintf fmt "@[<v>") fmtopt;
   Callgraph.Uses.iter_in_rev_order
     (fun kf ->
-       if !Db.Value.is_called kf then
+       if Eva.Results.is_called kf then
          let header fmt =
            Format.fprintf fmt "Function %a:" Kernel_function.pretty kf
          in
@@ -101,13 +101,11 @@ let print_calldeps () =
       if !Db.Value.no_results (Kernel_function.get_definition caller)
       then "<unknown>", funtype
       else
-        try
-          let set = Db.Value.call_to_kernel_function s in
-          let kf = Kernel_function.Hptset.choose set in
+        match Eva.Results.callee s with
+        | kf :: _ ->
           Pretty_utils.to_string Kernel_function.pretty kf,
           Kernel_function.get_type kf
-        with
-        | Not_found ->
+        | [] ->
           From_parameters.fatal
             ~source:(fst (Cil_datatype.Stmt.loc s))
             "Invalid call %a@." Printer.pp_stmt s
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index ecc6d928ac22807e6ba6d5430d6e41d8a68f47b8..a4f0a3e3065f582eab966749d0c87bcdb2265d98 100644
--- a/src/plugins/from/functionwise.ml
+++ b/src/plugins/from/functionwise.ml
@@ -95,7 +95,7 @@ let force_compute_all () =
   Eva.Analysis.compute ();
   Callgraph.Uses.iter_in_rev_order
     (fun kf ->
-       if Kernel_function.is_definition kf && !Db.Value.is_called kf
+       if Kernel_function.is_definition kf && Eva.Results.is_called kf
        then !Db.From.compute kf)
 
 (* Db Registration for function-wise from *)
diff --git a/src/plugins/metrics/metrics_pivot.ml b/src/plugins/metrics/metrics_pivot.ml
index 2f943abca822231740f08df2e923ac6a2e532022..28ff05163be8866c904344217931cfcdcd5850e7 100644
--- a/src/plugins/metrics/metrics_pivot.ml
+++ b/src/plugins/metrics/metrics_pivot.ml
@@ -29,7 +29,7 @@ module PivotSourceState =
     (Datatype.List(Datatype.String))
     (struct
       let name = "PivotSourceState"
-      let dependencies = [ Ast.self; Db.Value.self; Property_status.self;
+      let dependencies = [ Ast.self; Eva.Analysis.self; Property_status.self;
                            Messages.self ]
     end)
 
diff --git a/src/plugins/pdg/annot.ml b/src/plugins/pdg/annot.ml
index 7bfa2eb708f0c78b5f86acaab1328a9f02527c47..d76dc95c38da8546bce3569b83ddcadbb3fbfa54 100644
--- a/src/plugins/pdg/annot.ml
+++ b/src/plugins/pdg/annot.ml
@@ -106,7 +106,7 @@ let find_code_annot_nodes pdg stmt annot =
   Pdg_parameters.debug "[pdg:annotation] CodeAnnot-%d stmt %d : %a @."
     annot.annot_id stmt.sid
     Printer.pp_code_annotation annot;
-  if Db.Value.is_reachable_stmt stmt then
+  if Eva.Results.is_reachable stmt then
     begin
       let kf =  PdgTypes.Pdg.get_kf pdg in
       let (data_info, decl_label_info), pragmas =
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index 6b5be2c31fa08deedea5532993759c686f387bb7..d0df6abb5b2ed376ab6186867a5170e3ee651e0f 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -465,12 +465,20 @@ let create_fun_output_node pdg state dpds =
   | Some state -> add_dpds pdg new_node Dpd.Data state dpds
   | None -> (* return is unreachable *) ()
 
+let find_return_lval kf =
+  let stmt = Kernel_function.find_return kf in
+  match stmt with
+  | { skind = Return (Some {enode = Lval lval}, _) } -> stmt, lval
+  | _ -> assert false
+
 (** add a node corresponding to the returned value. *)
 let add_retres pdg state ret_stmt retres_loc_dpds retres_decls =
   let key_return = Key.stmt_key ret_stmt in
   let return_node = add_elem pdg key_return in
-  let retres_loc = Db.Value.find_return_loc pdg.fct in
-  let retres = Locations.(enumerate_valid_bits Read retres_loc) in
+  let retres =
+    let stmt, lval = find_return_lval pdg.fct in
+    Eva.Results.(before stmt |> eval_address ~for_writing:false lval |> as_zone)
+  in
   add_dpds pdg return_node  Dpd.Data state retres_loc_dpds;
   add_decl_dpds pdg return_node Dpd.Data retres_decls;
   let new_state = Pdg_state.add_loc_node state ~exact:true retres return_node in
@@ -600,11 +608,11 @@ let finalize_pdg pdg from_opt =
     = location + exact + dependencies + declarations *)
 let get_lval_infos lval stmt =
   let decl = Cil.extract_varinfos_from_lval lval in
-  let state = Db.Value.get_stmt_state stmt in
-  let dpds, z_loc, exact =
-    !Db.Value.lval_to_zone_with_deps_state
-      state ~deps:(Some Locations.Zone.bottom) ~for_writing:true lval
-  in
+  let request = Eva.Results.before stmt in
+  let address = Eva.Results.eval_address ~for_writing:true lval request in
+  let z_loc = Eva.Results.as_zone address in
+  let exact = Eva.Results.is_singleton address in
+  let dpds = Eva.Results.address_deps lval request in
   (z_loc, exact, dpds, decl)
 
 (** process assignment {v lval = exp; v}
@@ -700,15 +708,17 @@ let process_call pdg state stmt lvaloption funcexp argl _loc =
   ignore (add_elem pdg (Key.call_ctrl_key stmt));
   let arg_nodes = process_args pdg state_before_call stmt argl in
   let state_with_args = state in
-  let funcexp_dpds, called_functions =
-    !Db.Value.expr_to_kernel_function
-      (Kstmt stmt) ~deps:(Some Locations.Zone.bottom) funcexp
+  let called_functions = Eva.Results.callee stmt in
+  let funcexp_dpds =
+    match funcexp.enode with
+    | Lval lval -> Eva.Results.(before stmt |> address_deps lval)
+    | _ -> assert false
   in
   let mixed_froms =
     try let froms = !Db.From.Callwise.find (Kstmt stmt) in Some froms
     with Not_found -> None (* don't have callwise analysis (-calldeps option) *)
   in
-  let process_simple_call called_kf acc =
+  let process_simple_call acc called_kf =
     let state_with_inputs =
       process_call_params pdg state_with_args stmt called_kf arg_nodes
     in
@@ -724,7 +734,7 @@ let process_call pdg state stmt lvaloption funcexp argl _loc =
     in r :: acc
   in
   let state_for_each_call =
-    Kernel_function.Hptset.fold process_simple_call called_functions []
+    List.fold_left process_simple_call [] called_functions
   in
   let new_state =
     match state_for_each_call with
@@ -755,7 +765,7 @@ let process_condition ctrl_dpds_infos pdg state stmt condition =
   let decls_cond = Cil.extract_varinfos_from_exp condition in
 
   let controlled_stmts = CtrlDpds.get_if_controlled_stmts ctrl_dpds_infos stmt in
-  let go_then, go_else = Db.Value.condition_truth_value stmt in
+  let go_then, go_else = Eva.Results.condition_truth_value stmt in
   let real = go_then && go_else (* real dpd if we can go in both branches *) in
   if not real then
     debug
@@ -773,7 +783,7 @@ let process_jump_stmt pdg ctrl_dpds_infos jump =
   let controlled_stmts =
     CtrlDpds.get_jump_controlled_stmts ctrl_dpds_infos jump
   in
-  let real = Db.Value.is_reachable_stmt jump in
+  let real = Eva.Results.is_reachable jump in
   if not real then
     debug "[process_jump_stmt] stmt %d is not a real jump@." jump.sid;
   process_jump pdg jump (real, controlled_stmts)
@@ -791,7 +801,7 @@ let process_loop_stmt pdg ctrl_dpds_infos loop =
   let controlled_stmts =
     CtrlDpds.get_loop_controlled_stmts ctrl_dpds_infos loop
   in
-  let real_loop = List.exists (Db.Value.is_reachable_stmt) back_edges in
+  let real_loop = List.exists Eva.Results.is_reachable back_edges in
   if not real_loop then
     debug "[process_loop_stmt] stmt %d is not a real loop@." loop.sid;
   process_jump pdg loop (real_loop, controlled_stmts)
@@ -812,11 +822,11 @@ let process_return _current_function pdg state stmt ret_exp =
       add_retres pdg state stmt loc_exp decls_exp
     | None ->
       let controlled_stmt = Cil_datatype.Stmt.Hptset.empty in
-      let real = Db.Value.is_reachable_stmt stmt in
+      let real = Eva.Results.is_reachable stmt in
       process_jump pdg stmt (real, controlled_stmt);
       state
   in
-  if Db.Value.is_reachable_stmt stmt then
+  if Eva.Results.is_reachable stmt then
     Pdg_state.store_last_state pdg.states last_state
 
 module Computer
@@ -866,7 +876,7 @@ module Computer
     Db.yield ();
     pdg_debug "doInstr sid:%d : %a" stmt.sid Printer.pp_instr instr;
     match instr with
-    | _ when not (Db.Value.is_reachable_stmt stmt) ->
+    | _ when not (Eva.Results.is_reachable stmt) ->
       pdg_debug "stmt sid:%d is unreachable : skip.@." stmt.sid ;
       Pdg_state.bottom
     | Local_init (v, AssignInit i, _) ->
@@ -977,7 +987,7 @@ let compute_pdg_for_f kf =
           let ctrl_dpds_infos = ctrl_dpds_infos
         end)
       in
-      if Db.Value.is_reachable_stmt start then
+      if Eva.Results.is_reachable start then
         begin
           let module Compute = Dataflows.Simple_forward(Fenv)(Computer) in
           Array.iteri (fun ord value ->
diff --git a/src/plugins/pdg/marks.ml b/src/plugins/pdg/marks.ml
index 628611b95e3219ef821b9c759a298aab848d9fa3..272b5b1ad9fe0928b90ed766e1c06a0345f5afcc 100644
--- a/src/plugins/pdg/marks.ml
+++ b/src/plugins/pdg/marks.ml
@@ -63,7 +63,7 @@ let translate_in_marks pdg_called in_new_marks
   let translate pdg rqs call =
     in_marks_to_caller pdg call (m2m (Some call) pdg) ~rqs in_new_marks
   in
-  let build rqs (caller, _) =
+  let build rqs caller =
     let pdg_caller = !Db.Pdg.get caller in
     let caller_rqs =
       try
@@ -77,8 +77,7 @@ let translate_in_marks pdg_called in_new_marks
     in
     (pdg_caller, caller_rqs)::rqs
   in
-  let res = List.fold_left build other_rqs (!Db.Value.callers kf_called) in
-  res
+  List.fold_left build other_rqs (Eva.Results.callers kf_called)
 
 let call_out_marks_to_called called_pdg m2m ?(rqs=[]) out_marks =
   let build rqs (out_key, m) =
@@ -98,7 +97,7 @@ let call_out_marks_to_called called_pdg m2m ?(rqs=[]) out_marks =
   List.fold_left build rqs out_marks
 
 let translate_out_mark _pdg m2m other_rqs (call, l) =
-  let add_list l_out_m called_kf rqs  =
+  let add_list l_out_m rqs called_kf  =
     let called_pdg = !Db.Pdg.get called_kf in
     let m2m = m2m (Some call) called_pdg in
     try
@@ -111,8 +110,8 @@ let translate_out_mark _pdg m2m other_rqs (call, l) =
        * *)
       rqs
   in
-  let all_called = Db.Value.call_to_kernel_function call in
-  Kernel_function.Hptset.fold (add_list l)  all_called other_rqs
+  let all_called = Eva.Results.callee call in
+  List.fold_left (add_list l) other_rqs all_called
 
 (** [add_new_marks_to_rqs pdg new_marks other_rqs] translates [new_marks]
  * that were computed during intraprocedural propagation into requests,
diff --git a/src/plugins/pdg/register.ml b/src/plugins/pdg/register.ml
index ff00ddbddf132d7f679ae9f6080ce314e82c7160..4f707e7ffeb43572c405893f74411acb98b2b560 100644
--- a/src/plugins/pdg/register.ml
+++ b/src/plugins/pdg/register.ml
@@ -123,7 +123,7 @@ let () = Pdg_parameters.BuildAll.set_output_dependencies deps
 
 let compute_for_kf kf =
   let all = Pdg_parameters.BuildAll.get () in
-  (all && !Db.Value.is_called kf) ||
+  (all && Eva.Results.is_called kf) ||
   Kernel_function.Set.mem kf (Pdg_parameters.BuildFct.get ())
 
 let compute () =
diff --git a/src/plugins/pdg/sets.ml b/src/plugins/pdg/sets.ml
index 9fff226ac9021220f29429141aad38420c15d95c..89b83596775910a2d19721723910ccdd42e323e1 100644
--- a/src/plugins/pdg/sets.ml
+++ b/src/plugins/pdg/sets.ml
@@ -215,7 +215,7 @@ let find_call_stmts kf ~caller =
   match
     List.filter
       (fun (f, _) -> Kernel_function.equal f caller)
-      (!Db.Value.callers kf)
+      (Eva.Results.callsites kf)
   with
   | [] -> []
   | [ _, callsites ] -> assert (callsites <> []); callsites
diff --git a/src/plugins/postdominators/compute.ml b/src/plugins/postdominators/compute.ml
index d39e990b9dc6613be513aa5d2a42f825a005386f..8126dda260958b2954f0aaf4e52df515036e9c3a 100644
--- a/src/plugins/postdominators/compute.ml
+++ b/src/plugins/postdominators/compute.ml
@@ -258,8 +258,7 @@ include
       let is_accessible = Eva.Results.is_reachable
       let dependencies = [ Eva.Analysis.self ]
       let name = "value"
-      let eval_cond stmt _e =
-        Db.Value.condition_truth_value stmt
+      let eval_cond stmt _e = Eva.Results.condition_truth_value stmt
     end)
     (Db.PostdominatorsValue)
 
diff --git a/src/plugins/scope/zones.ml b/src/plugins/scope/zones.ml
index 5106189940f635d0cbf75b96a254c62e11cc9d94..aa02df158d8b3d246e59e501748f8fdf5dd3ae08 100644
--- a/src/plugins/scope/zones.ml
+++ b/src/plugins/scope/zones.ml
@@ -65,11 +65,11 @@ let compute_new_data old_zone l_zone l_dpds exact r_dpds =
   else (false, old_zone)
 
 let get_lval_zones ~for_writing stmt lval =
-  let state = Db.Value.get_stmt_state stmt in
-  let dpds, zone, exact =
-    !Db.Value.lval_to_zone_with_deps_state
-      state ~deps:(Some Locations.Zone.bottom) ~for_writing lval
-  in
+  let request = Eva.Results.before stmt in
+  let address = Eva.Results.eval_address ~for_writing lval request in
+  let zone = Eva.Results.as_zone address in
+  let exact = Eva.Results.is_singleton address in
+  let dpds = Eva.Results.address_deps lval request in
   dpds, exact, zone
 
 (* the call result can be processed like a normal assignment *)
diff --git a/src/plugins/slicing/slicingTransform.ml b/src/plugins/slicing/slicingTransform.ml
index 8fe9a26d5b60bd0222ce0d623b4ac0c87bd01c35..da5c14f22b2a58f2bb6a5d3a09e37611a204211b 100644
--- a/src/plugins/slicing/slicingTransform.ml
+++ b/src/plugins/slicing/slicingTransform.ml
@@ -449,7 +449,7 @@ module Visibility (SliceName : sig
     info
 
   let cond_edge_visible _ff_opt s =
-    Db.Value.condition_truth_value s
+    Eva.Results.condition_truth_value s
 
 end
 
diff --git a/src/plugins/sparecode/transform.ml b/src/plugins/sparecode/transform.ml
index dd67f76849324e533f84ca8f79ec551b87078fb0..e2280ec81b2c4ad240ddcd1902c29356572e55d9 100644
--- a/src/plugins/sparecode/transform.ml
+++ b/src/plugins/sparecode/transform.ml
@@ -155,7 +155,7 @@ module BoolInfo = struct
     with Kernel_function.No_Statement -> true
 
   let cond_edge_visible _ s =
-    Db.Value.condition_truth_value s
+    Eva.Results.condition_truth_value s
 end
 
 module Info = Filter.F (BoolInfo)
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index 34883ace8adb8f69fb01045657630c21715090d6..6e92b4373d7234f4919ff260b91e34f67b68df90 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -682,6 +682,7 @@ let is_reachable_kinstr kinstr =
   let module M = Make () in
   M.is_reachable (before_kinstr kinstr)
 
+let condition_truth_value = Db.Value.condition_truth_value
 
 (* Callers / callsites *)
 
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index a14dd721dea46ae8235d8920d4808ea5ddd6e1fa..a35f29f8d30cc08b81ea9531ead9184e34b242df 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -275,6 +275,10 @@ val is_reachable : Cil_types.stmt -> bool
     the main function has been analyzed for [Kglobal]. *)
 val is_reachable_kinstr : Cil_types.kinstr -> bool
 
+val condition_truth_value: Cil_types.stmt -> bool * bool
+(** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
+    (resp. snd) is true if and only if the condition of the 'if' has been
+    evaluated to true (resp. false) at least once during the analysis. *)
 
 (*** Callers / Callees / Callsites *)
 
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 9d9436836ec6a35e0df4dc837eae0c634d9def9f..7b86d44704aec8a4d451079e449bfd9320966bd0 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -364,7 +364,6 @@
 [eva] Done for function copy_0
 [eva] Recording results for main_all
 [from] Computing for function main_all
-[from] Non-terminating function main_all (no dependencies)
 [from] Done for function main_all
 [eva] done for function main_all
 [scope:rm_asserts] removing 1 assertion(s)
diff --git a/tests/pdg/oracle/bts1194.res.oracle b/tests/pdg/oracle/bts1194.res.oracle
index 47e6cda07df505a5319c1e6a660712eb26020172..145aeb752d3a920752391a5eaaa261f9a2e3e284 100644
--- a/tests/pdg/oracle/bts1194.res.oracle
+++ b/tests/pdg/oracle/bts1194.res.oracle
@@ -24,7 +24,6 @@
 [eva] bts1194.c:20: function g: no state left, postcondition got status valid.
 [eva] Recording results for g
 [from] Computing for function g
-[from] Non-terminating function g (no dependencies)
 [from] Done for function g
 [eva] Done for function g
 [eva] Recording results for h
diff --git a/tests/pdg/oracle/top_pdg_input.res.oracle b/tests/pdg/oracle/top_pdg_input.res.oracle
index 72f904673274a5504962f083902fd9626ec5e46a..4560b0573061290b9ec67795f6988d164a980fc6 100644
--- a/tests/pdg/oracle/top_pdg_input.res.oracle
+++ b/tests/pdg/oracle/top_pdg_input.res.oracle
@@ -256,17 +256,12 @@ Cannot filter: dumping raw memory (including unchanged variables)
 [from] Done for function fun_asm
 [from] Computing for function main_asm
 [from] Done for function main_asm
-[from] Computing for function no_results
-[from] Done for function no_results
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
 [from] Function fun_asm:
   \result FROM i
 [from] Function main_asm:
   \result FROM \nothing
-[from] Function no_results:
-  FROMTOP
-  \result FROM ANYTHING(origin:Unknown)
 [from] ====== END OF DEPENDENCIES ======
 [inout] Out (internal) for function fun_asm:
     __retres
@@ -285,8 +280,6 @@ Cannot filter: dumping raw memory (including unchanged variables)
 [pdg] done for function fun_asm
 [pdg] computing for function main_asm
 [pdg] done for function main_asm
-[pdg] computing for function no_results
-[pdg] Top for function no_results
 [pdg] ====== PDG GRAPH COMPUTED ======
 [pdg] PDG for fun_asm
  {n47}: InCtrl
@@ -333,5 +326,3 @@ Cannot filter: dumping raw memory (including unchanged variables)
    -[--d]-> 61
  {n63}: OutRet
    -[--d]-> 62
-[pdg] PDG for no_results
- Top PDG
diff --git a/tests/slicing/oracle/min_call.res.oracle b/tests/slicing/oracle/min_call.res.oracle
index 858153ee93740c28d7b7379d50f8de6beca11e87..f3607c3ab3b4940722b6795cd9097a58361a414b 100644
--- a/tests/slicing/oracle/min_call.res.oracle
+++ b/tests/slicing/oracle/min_call.res.oracle
@@ -104,10 +104,10 @@
 [slicing] applying all slicing requests...
 [slicing] applying 1 actions...
 [slicing] applying actions: 1/1...
-[pdg] computing for function f
-[pdg] done for function f
 [pdg] computing for function g
 [pdg] done for function g
+[pdg] computing for function f
+[pdg] done for function f
 Project1 - result1 :
 [slicing] exporting project to 'Sliced code'...
 [slicing] applying all slicing requests...
@@ -464,14 +464,14 @@ void f_slice_1(void)
 [slicing] applying all slicing requests...
 [slicing] applying 0 actions...
 Slicing project worklist [default] =
-[f = (n:26 ,<[acd], [---]>)(n:33 ,<[acd], [---]>)(n:41 ,<[acd], [---]>)][g = (n:60 ,
+[f = (n:45 ,<[acd], [---]>)(n:52 ,<[acd], [---]>)(n:60 ,<[acd], [---]>)][g = (n:27 ,
 <[acd],
 [---]>)]
 
 Slicing project worklist [default] =
-[f_slice_1 = choose_call for call 17][f_slice_1 = choose_call for call 16][f_slice_1 = choose_call for call 15][g = propagate (n:68 ,
+[f_slice_1 = choose_call for call 17][f_slice_1 = choose_call for call 16][f_slice_1 = choose_call for call 15][g = propagate (n:35 ,
 <[acd],
-[---]>)][Appli : calls to f][g = (n:60 ,<[acd], [---]>)]
+[---]>)][Appli : calls to f][g = (n:27 ,<[acd], [---]>)]
 
 [slicing] applying all slicing requests...
 [slicing] applying 6 actions...
diff --git a/tests/sparecode/oracle/bts334.2.res.oracle b/tests/sparecode/oracle/bts334.2.res.oracle
index 06b83c96a7ef143df4a3b8ca490632b2bcbb2f78..46154e7440ca51b5e742d0548aad9600d1ff5c1a 100644
--- a/tests/sparecode/oracle/bts334.2.res.oracle
+++ b/tests/sparecode/oracle/bts334.2.res.oracle
@@ -97,7 +97,6 @@
 [eva] Done for function loop_body
 [eva] Recording results for process
 [from] Computing for function process
-[from] Non-terminating function process (no dependencies)
 [from] Done for function process
 [eva] Done for function process
 [eva] Recording results for main_init
diff --git a/tests/value/oracle/loopfun.0.res.oracle b/tests/value/oracle/loopfun.0.res.oracle
index c7543f7da625ee78a4aa75d0e958968a19680090..02f251803d78aa639a83968d99ce891aa2168226 100644
--- a/tests/value/oracle/loopfun.0.res.oracle
+++ b/tests/value/oracle/loopfun.0.res.oracle
@@ -42,23 +42,23 @@
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
-[from] Computing for function main2
-[from] Done for function main2
-[from] Computing for function test
-[from] Done for function test
 [from] Computing for function main
 [from] Done for function main
+[from] Computing for function test
+[from] Done for function test
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
-[from] Function main2:
-  FROMTOP
-[from] Function test:
+[from] Function main:
   FROMTOP
   \result FROM ANYTHING(origin:Unknown)
-[from] Function main:
+[from] Function test:
   FROMTOP
   \result FROM ANYTHING(origin:Unknown)
 [from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main:
+    ANYTHING(origin:Unknown)
+[inout] Inputs for function main:
+    ANYTHING(origin:Unknown)
 [inout] Out (internal) for function main2:
     \nothing
 [inout] Inputs for function main2:
@@ -67,7 +67,3 @@
     tmp; a
 [inout] Inputs for function test:
     a
-[inout] Out (internal) for function main:
-    ANYTHING(origin:Unknown)
-[inout] Inputs for function main:
-    ANYTHING(origin:Unknown)