The use of SAT-solving is of course the essence of MACE-style model-finding, but the difference here is that we do not simply work with the ground instances of the input theory, T, over a fixed set of constants.