Patent ID: 7925476

Claim:
In a computing environment comprising at least one processor operatively coupled to system memory, a method for combining the models of a plurality of theory solvers in order to produce a model which is satisfiable by each of the plurality of theory solvers, the method comprising: a processor accessing a model for a first theory solver which is satisfiable in the first theory solver; the processor determining a set of one or more equalities which are implied by the model, comprising determining that each equality in the set of one or more equalities include a plurality of symbols that have the same value in the model; the processor determining that at least one of the set of one or more equalities are not compatible with a second theory solver, comprising communicating one or more equalities from the set of one or more equalities to the second theory solver; and the processor updating the model in accordance with at least one equality determined not to be compatible with the second solver to create an updated model, wherein updating comprises backtracking to fix values assigned in the model which imply equalities which are not compatible with the second theory solver, such that the updated model is satisfiable in both the first theory solver and the second theory solver.