Finite Model Finding in SMT

SMT solvers have been used successfully as reasoning engines for automated verification. Current techniques for dealing with quantified formulas in SMT are generally incomplete, forcing SMT solvers to report “unknown” when they fail to prove the unsatisfiability of a formula with quantifiers. This inability to return counter-models limits their usefulness in applications that produce quantified verification conditions. We present a novel finite model finding method that reduces these limitations in the case of quantifiers ranging over free sorts. Our method contrasts with previous approaches for finite model finding in first-order logic by not relying on the introduction of

domain constants

for the free sorts and by being fully integrated into the general architecture used by most SMT solvers. This integration is achieved through the addition of a novel solver for sort cardinality constraints and a module for quantifier instantiation over finite domains. Initial experiments with verification conditions generated from a deductive verification tool developed at Intel Corp. show that our approach compares quite favorably with the state of the art in SMT.