anchor.diff:          @[Term.CheckSat]
           @suffix in
   
  -    let check (p:decl) =
  +    let check (p:decl) =        
           let cached_config =
               match !fuel_trace with 
  -            | ReplayFuelTrace (hd::tl) ->
  +            | ReplayFuelTrace (fname, hd::tl) ->
                   let fuel, ifuel = hd in
  -                fuel_trace := ReplayFuelTrace tl;
  -                Some (fuel, ifuel)
  +                fuel_trace := ReplayFuelTrace (fname, tl);
  +                Some (fname, fuel, ifuel)
               | _ ->
                   None
           in
           let initial_config = 
               match cached_config with 
  -            | Some x -> x
  +            | Some (_, fuel, ifuel) -> (fuel, ifuel)
               | None -> (!Options.initial_fuel, !Options.initial_ifuel) 
           in
           let alt_configs = 
  
positive.code:     | Some state ->
          let digest = md5_of_file src_fn in
          if state.identity.source_digest = digest then
              fuel_trace := ReplayFuelTrace state.fuels
          else
              fuel_trace := RecordFuelTrace []
      | None ->
  
negative.code: type fuel_trace_status =
      | FuelTraceUnavailable
      | RecordFuelTrace of list<(int * int)>
      | ReplayFuelTrace of (string * list<(int * int)>)
  
  let fuel_trace : ref<fuel_trace_status> = Util.mk_ref <| FuelTraceUnavailable
  
  