  We investigate the domain of satisfiable formulas in satisfiability modulo
theories (SMT), in particular, automatic generation of a multitude of
satisfying assignments to such formulas. Despite the long and successful
history of SMT in model checking and formal verification, this aspect is
relatively under-explored. Prior work exists for generating such assignments,
or samples, for Boolean formulas and for quantifier-free first-order formulas
involving bit-vectors, arrays, and uninterpreted functions (QF_AUFBV). We
propose a new approach that is suitable for a theory T of integer arithmetic
and to T with arrays and uninterpreted functions. The approach involves
reducing the general sampling problem to a simpler instance of sampling from a
set of independent intervals, which can be done efficiently. Such reduction is
carried out by expanding a single model - a seed - using top-down propagation
of constraints along the original first-order formula.
