anchor.diff:      let s = Util.concat_l "," <| List.sortWith String.compare digests in
       digest_of_string s
   
  -let initialize_fuel_trace src_fn deps : unit =
  -    let norm_src_fn = Util.normalize_file_path src_fn in
  -    let val_fn = format_fuel_trace_file_name norm_src_fn in
  -    match Util.load_value_from_file val_fn with
  -    | Some state ->
  -        let means, validated = 
  -            if !Options.explicit_deps then
  -                (* we're unable to compute the transitive digest when `--explicit_deps` is specified. *)
  -                let expected = Util.digest_of_file norm_src_fn in
  -                ("Module", state.identity.module_digest = expected)
  -            else 
  -                ("Transitive",
  -                    begin
  -                        match state.identity.transitive_digest with
  -                        | None ->
  -                            false
  -                        | Some d ->
  -                            let expected = compute_transitive_digest norm_src_fn deps in
  -                            d = expected
  -                    end)
  -        in
  -        if validated then
  -            begin if !Options.print_fuels then
  -                    Util.print2 "(%s) %s digest is valid.\n" norm_src_fn means
  -                else
  -                    ();
  -                fuel_trace := ReplayFuelTrace (val_fn, state.fuels)
  -            end
  -        else
  -            begin if !Options.print_fuels then
  -                  Util.print2 "(%s) %s digest is invalid.\n" norm_src_fn means
  -              else
  -                  ();
  -              fuel_trace := RecordFuelTrace []
  -            end
  -    | None ->
  -        if !Options.print_fuels then
  -            Util.print1 "(%s) Unable to read cached fuel trace.\n" norm_src_fn
  -        else
  -            ();
  -        fuel_trace := RecordFuelTrace []
  -
  -let finalize_fuel_trace src_fn deps : unit =
  -    begin match !fuel_trace with
  -    | ReplayFuelTrace _ 
  -    (* failure to verify *)
  -    | FuelTraceUnavailable 
  -    (* verification not performed *)
  -    | RecordFuelTrace [] ->
  -        ()
  -    (* verification successful *)
  -    | RecordFuelTrace l ->
  -        let val_fn = format_fuel_trace_file_name src_fn in
  -        let xd = 
  -            (* we're unable to compute the transitive digest when `--explicit_deps` is specified. *)
  -            if !Options.explicit_deps then
  -                None
  -            else
  -                Some <| compute_transitive_digest src_fn deps
  -        in
  -        let state = {
  -            identity = {
  -                module_digest = Util.digest_of_file src_fn;
  -                transitive_digest = xd 
  -            };
  -            fuels = l
  -        }
  -        in
  -        Util.save_value_to_file val_fn state
  -    end;
  -    fuel_trace := FuelTraceUnavailable
  +let is_replaying_fuel_trace () =
  +  match !fuel_trace with 
  +  | ReplayFuelTrace _ ->
  +    true
  +  | _ ->
  +    false
   
   (****************************************************************************)
   (* Z3 Specifics                                                             *)
  
positive.code:   if !Options.logQueries then log_query fresh input;
    enqueue fresh ({job=z3_job fresh label_messages input; callback=cb})
  
  
negative.code: let ctr = Util.mk_ref (-1)
  
  let new_proc () =
    let timeout = 
      if is_replaying_fuel_trace () then
        None
      else
        Some !Options.z3timeout
    in
    new_z3proc (Util.format1 "bg-%s" (incr ctr; !ctr |> string_of_int)) timeout
  
  let z3proc () =
    if !the_z3proc = None then
  