Disequality Management in Integer Difference Logic via Finite Instantiations1
Hyondeuk Kim, HoonSang Jin, Fabio Somenzi · Journal on Satisfiability Boolean Modeling and Computation · 2007
The last few years have seen the advent of a new breed of decision procedures for various fragments of first-order logic based on propositional abstraction. A lazy satisfiability checker for a given fragment of first-order logic invokes a theory-spec