Abstract: Satisfiability modulo theories (SMT) play a key role in verification applications. A crucial SMT problem is to combine separate theory solvers for the union of theories. In previous work, the simplex method is used to determine the solvability of constraint systems and the equalities implied by constraint systems are detected by a multitude of applications of the dual simplex method. We present an effective simplex tableau-based method to identify all implicit equalities such that the simplex method is harnessed to an irreducible minimum. Experimental results show that the method is feasible and effective.

Key words: Model checking, Satisfiability modulo theories (SMT), Linear arithmetic

Please provide your name, email address and a comment

Your Name: Affili: E-Mail Address:

Comment (Please comment in English):


Verification Code(click to change a pic):