Tools that explore very large state spaces to find bugs, e.g., when
model checking, or to find solutions, e.g., when constraint solving,
can take a considerable amount of time before the search terminates,
and the user may not get useful feedback on the state of the search
during that time. Our focus is a tool that solves imperative
constraints to provide automated test input generation for systematic
testing. Specifically, we introduce a technique to quantify the
exploration of Korat, a well-known tool that explores the bounded
space of all candidate inputs and enumerates desired inputs that
satisfy given constraints. Our technique quantifies the size of the
input space as it is explored by the Korat search, and provides the
user exact information on the size of the remaining input space. In
addition, it allows studying key characteristics of the search, such
as the distribution of solutions as the search finds them. We
implement the technique as a listener for the Korat search, and
present initial experimental results using it.