We consider the problem of efficiently computing models for
satisfiable constraints, in the presence of complex background
theories such as floating-point arithmetic. Model construction has
various applications, for instance the automatic generation of test
inputs. It is well-known that naive encoding of constraints into
simpler theories (for instance, bit-vectors or propositional logic)
can lead to a drastic increase in size, and be unsatisfactory in terms
of memory and runtime needed for model construction. We define a
framework for systematic application of approximations in order to
speed up model construction. Our method is more general than previous
techniques in the sense that approximations that are neither under-
nor over-approximations can be used, and shows promising results in
practice.