anchor.diff:          mark_empty -> eq(NextRebuildT2, incremental);
           _ -> eq(NextRebuildT2, full)
       end;
  +%% After a comparison, check against the results against
  +%% the ETS table containing the *snapshot* copies.
  +postcondition(_S,{call, _, local_compare, _},  Result) ->
  +    Expect = expect_compare(),
  +    eq(Expect, lists:sort(Result));	
   postcondition(_S,{call,_,_,_},_R) ->
       true.
   
  -next_state(S,_R,{call, _, start, [Params,_,_]}) ->
  -    S#state{started = true, params = Params};
  -next_state(S,_V,{call, _, write, [t1, Objects]}) ->
  -    S#state{only1=keymerge(Objects, S#state.only1)};
  -next_state(S,_V,{call, _, write, [t2, Objects]}) ->
  -    S#state{only2=keymerge(Objects, S#state.only2)};
  -next_state(S,_R,{call, _, write_both, [Objects]}) ->
  -    S#state{only1=keymerge(Objects, S#state.only1),
  -            only2=keymerge(Objects, S#state.only2)};
  -next_state(S,_V,{call, _, delete, [t1, Key]}) ->
  -    S#state{only1=lists:keydelete(Key, 1, S#state.only1)};
  -next_state(S,_V,{call, _, delete, [t2, Key]}) ->
  -    S#state{only2=lists:keydelete(Key, 1, S#state.only2)};
  -next_state(S,_R,{call, _, delete_both, [Key]}) ->
  -    S#state{only1=lists:keydelete(Key, 1, S#state.only1),
  -            only2=lists:keydelete(Key, 1, S#state.only2)};
  -next_state(S,_R,{call, _, reopen_tree, _A}) ->
  -    S;
  -next_state(S,_R,{call, _, unsafe_close, _A}) ->
  -    S;
  -next_state(S,_R,{call, _, rehash_tree, _A}) ->
  -    S;
  -next_state(S,_R,{call, _, reconcile, []}) ->
  -    Keys = keymerge(S),
  -    S#state{only1 = Keys,
  -            only2 = Keys};
  -next_state(S,_R,{call, _, update_tree, _A}) ->
  +next_state(S,R,{call, _, start, [Params,_ExtraIds,_,_]}) ->
  +    %% Start returns the TreeId used, stick in the state
  +    %% as no hashtree:tree_id call yet.
  +    S#state{started = true, tree_id = R, params = Params};
  +next_state(S,_V,{call, _, update_tree, [t1, _]}) ->
  +    S#state{snap1 = updated};
  +next_state(S,_V,{call, _, update_tree, [t2, _]}) ->
  +    S#state{snap2 = updated};
  +next_state(S,_V,{call, _, update_snapshot, [t1, _]}) ->
  +    S#state{snap1 = created};
  +next_state(S,_V,{call, _, update_snapshot, [t2, _]}) ->
  +    S#state{snap2 = created};
  +next_state(S,_V,{call, _, update_perform, [t1]}) ->
  +    S#state{snap1 = updated};
  +next_state(S,_V,{call, _, update_perform, [t2]}) ->
  +    S#state{snap2 = updated};
  +next_state(S,_V,{call, _, set_next_rebuild, [t1]}) ->
  +    S#state{snap1 = undefined};
  +next_state(S,_V,{call, _, set_next_rebuild, [t2]}) ->
  +    S#state{snap2 = undefined};
  +next_state(S,_V,{call, _, write, [_T, Objs]}) ->
  +    S#state{num_updates = S#state.num_updates + length(Objs)};
  +next_state(S,_R,{call, _, write_both, [Objs]}) ->
  +    S#state{num_updates = S#state.num_updates + 2*length(Objs)};
  +next_state(S,_V,{call, _, delete, _}) ->
  +    S#state{num_updates = S#state.num_updates + 1};
  +next_state(S,_R,{call, _, delete_both, _}) ->
  +    S#state{num_updates = S#state.num_updates + 2};
  +next_state(S,_R,{call, _, reopen_tree, [t1, _]}) ->
  +    S#state{snap1 = undefined};
  +next_state(S,_R,{call, _, reopen_tree, [t2, _]}) ->
  +    S#state{snap2 = undefined};
  +next_state(S,_R,{call, _, unsafe_close, [t1, _]}) ->
  +    S#state{snap1 = undefined};
  +next_state(S,_R,{call, _, unsafe_close, [t2, _]}) ->
  +    S#state{snap2 = undefined};
  +next_state(S,_R,{call, _, rehash_tree, [t1]}) ->
  +    S#state{snap1 = undefined};
  +next_state(S,_R,{call, _, rehash_tree, [t2]}) ->
  +    S#state{snap2 = undefined};
  +next_state(S,_R,{call, _, local_compare, []}) ->
       S.
   
   prop_correct() ->
  -    ?FORALL(Cmds,non_empty(commands(?MODULE, #state{})),
  +    ?FORALL(Cmds,commands(?MODULE, #state{}),
               aggregate(command_names(Cmds),
                   begin
                       %%io:format(user, "Starting in ~p\n", [self()]),
  
positive.code:                     catch ets:delete(t1),
                      catch ets:delete(t2),
                      {_H,S,Res} = HSR = run_commands(?MODULE,Cmds),
                      pretty_commands(?MODULE, Cmds, HSR,
                                      ?WHENFAIL(
                                         begin
                                             catch hashtree:destroy(hashtree:close(get(t1))),
                                             catch hashtree:destroy(hashtree:close(get(t2)))
                                         end,
                              begin
                                      Unique1 = S#state.only1 -- S#state.only2,
                                      Unique2 = S#state.only2 -- S#state.only1,
                                      Expected =  [{missing, Key} || {Key, _} <-
                                          Unique2, not
                                          lists:keymember(Key, 1, S#state.only1)] ++
                                      [{remote_missing, Key} || {Key, _} <-
                                          Unique1, not
                                          lists:keymember(Key, 1, S#state.only2)] ++
                                      [{different, Key} || Key <-
                                          sets:to_list(sets:intersection(sets:from_list([Key
                                                          || {Key,_} <- Unique1]),
                                                  sets:from_list([Key || {Key,_}
                                                      <- Unique2])))],
  
                                  case S#state.started of
                                      false ->
                                          true;
                                      _ ->
                                          %% io:format("\nFinal update tree1:\n"),
                                          T10 = hashtree:update_tree(get(t1)),
                                          %% io:format("\nFinal update tree2:\n"),
                                          T20 = hashtree:update_tree(get(t2)),
  
                                          %% io:format("\nFinal compare:\n"),
                                          KeyDiff = hashtree:local_compare(T10, T20),
  
                                          D1 = try dump(T10) catch _:Err1 -> Err1 end,
                                          D2 = try dump(T20) catch _:Err2 -> Err2 end,
  
                                          T11 = hashtree:mark_clean_close({0,0}, T10),
                                          T21 = hashtree:mark_clean_close({0,0}, T20),
                                          catch hashtree:destroy(hashtree:close(T11)),
                                          catch hashtree:destroy(hashtree:close(T21)),
                                          {Segments, Width, MemLevels} = S#state.params,
  
                                          ?WHENFAIL(
                                             begin
                                                 eqc:format("only1:\n~p\n", [S#state.only1]),
                                                 eqc:format("only2:\n~p\n", [S#state.only2]),
                                                 eqc:format("t1:\n~p\n", [D1]),
                                                 eqc:format("t2:\n~p\n", [D2])
                                             end,
                                             collect(with_title(mem_levels), MemLevels,
                                             collect(with_title(segments), Segments,
                                             collect(with_title(width), Width,
                                             collect(with_title(length),
                                             length(S#state.only1) + length(S#state.only2),
                                                     conjunction([{cmds, equals(ok, Res)},
                                                                  {diff, equals(lists:usort(Expected),
                                                                                lists:usort(KeyDiff))}]))))))
                                  end
                              end
                                  ))
                          end)).
  
  dump(Tree) ->
      Fun = fun(Entries) ->
  
negative.code:                   end, Objects),
      ok.
  
  %% Call the other wrapper to write to both trees.
  %%
  write_both(Objects) ->
      write(t1, Objects),
      write(t2, Objects),
      ok.
  
  
  %% Wrap hashtree:delete to remove a key from a tree (and remove
  %% from the model tree).
  %%
  %% Keys do not need to be present to remove them from the AAE tree.
  delete(T, Key) ->
      put(T, hashtree:delete(Key, get(T))),
      ets:delete(T, Key),
      ok.
  
  %% Call the other wrapper to remove the key from both trees.
  delete_both(Key) ->
      delete(t1, Key),
      delete(t2, Key),
      ok.
  
  %% Trigger a rehash of the whole interior tree.  There is a potential
  %% race condition with update_snapshot that is avoided by this model,
  %% however if called during update_perform executing it will silently
  %% break multi_select_segment.
  rehash_tree(T) ->
      put(T, hashtree:rehash_tree(get(T))),
      ok.
  
  %% Flush, update tree, mark clean close, close and reopen the AAE tree.
  reopen_tree(T, TreeId) ->
      HT = hashtree:flush_buffer(get(T)),
      {Segments, Width, MemLevels} = {hashtree:segments(HT), hashtree:width(HT),
                                      hashtree:mem_levels(HT)},
      Path = hashtree:path(HT),
  
      UpdatedHT = hashtree:update_tree(HT),
      CleanClosedHT = hashtree:mark_clean_close(TreeId, UpdatedHT),
      hashtree:close(CleanClosedHT),
  
      T1 = hashtree:new(TreeId, [{segments, Segments},
                                {width, Width},
                                {mem_levels, MemLevels},
                                {segment_path, Path}]),
  
      put(T, hashtree:mark_open_and_check(TreeId, T1)),
      ok.
  
  %% Simulate an unsafe close.  This flushes the write buffer so that the
  %% model has a chance of knowing what the correct repairs should be.
  unsafe_close(T, TreeId) ->
      HT = get(T),
      {Segments, Width, MemLevels} = {hashtree:segments(HT), hashtree:width(HT),
                                      hashtree:mem_levels(HT)},
  