Fix hierarchical refinement fall-through into linear search

[shaobo-he]

Summary

When Z3-based variable refinement is disabled, Corral’s hierarchical refinement search was not used as the final refinement algorithm. Instead it:

1. ran hierarchical search and obtained a valid tracked set ec;
2. stored ec in refinementState.trackedTokens;
3. fell through into the older linear refinement search;
4. overwrote the hierarchical result with the linear result.

Corral therefore paid for hierarchical search plus linear search, and kept only the linear result.

This behavior has existed since the initial Corral check-in (2013) and is present on upstream master.

Root cause

In GeneralRefinementScheme.doRefinement():

if (useHierarchicalSearch)
{
    var ec = refinementLoop(...);
    refinementState.trackedTokens = ec;
}
// no return / else — falls through
var trackedVars = new HashSet<>(initialTrackedTokens);  // restarts from scratch
// ... linear loop ...
refinementState.trackedTokens = trackedVars;  // overwrites hierarchical result

The linear phase always restarts from initialTrackedTokens, not from ec. Hierarchical results were only used for a debug progress assert before being discarded.

When the fall-through occurs

useZ3Search == true
  → Z3 refinement → return   (default sequential path; no fall-through)

useZ3Search == false && useHierarchicalSearch == true
  → hierarchical → [was: linear overwrite] → now: return

useZ3Search == false && useHierarchicalSearch == false
  → linear only

useZ3Search is forced off when:

• VariableSlicing.EncounteredParallelAssignment is true; or
• the concurrent path constructs GeneralRefinementScheme with z3search=false.

Evidence this was unintentional

• Linear refinement does not seed from the hierarchical result.
• Historical doRefinement1() (labeled “For CADE 2011”) runs linear, hierarchical, and Z3 independently as timing alternatives and does not compose them.

Change

Two lines after hierarchical assigns trackedTokens = ec:

timeTaken = (DateTime.Now - startTime);
return;

Test plan

• Default path (Z3 when available): 49/49 regression pass
• Forced hierarchical path: outcomes match pre-fix (SAFE/UNSAFE), 49/49
• Parallel-assign cases (015/ParAssign1, ParAssign2): outcomes preserved; path queries drop (e.g. 12→9, 20→14)
• Across 41 refinement invocations under forced hierarchical: hierarchical and linear tracked-set sizes always matched (fall-through changed cost, not sets, on this suite)