Efficient decision procedures for arithmetic play a very important
role in formal verification. In practical examples, however,
arithmetic constraints are often mixed with constraints from other
theories like the theory of arrays, Boolean satisfiability (SAT),
bit-vectors, etc. Therefore, decision procedures for arithmetic are
especially useful in combination with other decision procedures. The
framework for such a combination is implemented at Stanford in the
tool called Cooperating Validity Checker (CVC).

This work augments CVC with a decision procedure for the theory of
mixed integer linear arithmetic based on the Omega-test [pugh91omega]
extended to be online and proof producing. These extensions are the
most important and challenging part of the work, and are necessary to
make the combination efficient in practice.