 An approach of great interest at solving SAT problems in first-order logic is Satisfiability Modulo Theory (SMT) where the interpretation of symbols in the problem’s formulation is constrained by a background theory. For example, in linear arithmetic the function symbols are restricted to + and −. As another example, in the extensional theory of arrays (McCarthy 1962) the array function read(a, i) returns the value of the array a at index i, and write(a, i, x) returns the array identical to a but where the value of a at i is x. More formally,