Approximate reachability techniques trade off accuracy for the
capacity to deal with bigger designs. Cho et al~\cite{cho} proposed
partitioning the set of state bits into mutually disjoint subsets and
doing symbolic forward reachability on the individual subsets to
obtain an overapproximation of the reachable state set. 
Recently~\cite{shankar} this was improved upon by dividing the
set of state bits into various subsets that could possibly overlap,
and doing symbolic reachability over the overlapping subsets. In this
paper, we further improve on this scheme by augmenting the set of state 
variables with auxiliary state variables. These auxiliary state variables 
are added to capture some important internal conditions in the combinational
logic. Approximate symbolic forward reachability on overlapping
subsets of this augmented set of state variables yields much tighter
approximations than earlier methods. We demonstrate the effectiveness
of this simple enhancement by reporting greatly improved results when
applied to several control modules from the I/O unit in the Stanford
FLASH Multiprocessor. We also present significant improvements on the
bigger ISCAS 89 benchmark circuits.