SMT solvers have traditionally been optimized for determining the satisfiability of a query as quickly as possible. However, they are increasingly being used in applications where the time required to determine satisfiability might not be the main concern, such as mining inductive invariants for safety proofs.
This paper studies how lookahead-inspired SMT solving, when made sufficiently efficient and integrated into a conflict-driven, clause learning SMT core, can be a valuable component in a portfolio for proof-based interpolation in model checking.
We implemented the algorithmic idea, called Picky CDCL, in the SMT solver OpenSMT and show its efficiency in the Horn solver Golem using a range of model checking approaches and in SMT proof validation applications.