We introduce an efficient decision procedure for the theory of equality based on finite instantiations. When using the finite instantiations method, it is a common practice to take a range of [1..n] (where n is the number of input nonBoolean variables) as the range for all nonBoolean variables, resulting in a statespace of nn. Although various attempts to minimize this range were made, typically they either required various restrictions on the investigated formulas or were not very effective. In many cases, the nn statespace cannot be handled by BDDbased tools within a reasonable amount of time. In this paper we show that significantly smaller domains can be algorithmically found, by analyzing the structure of the formula. We also show an upper bound for the statespace based on this analysis. This method enabled us to verify formulas containing hundreds of integer and floating point variables.
11th International conference on Computer Aided Verification