Computing with an SMT Solver

Nada Amin, Rustan Leino, Tiark Rompf

8th International Conference, TAP 2014, Held as Part of STAF 2014, York, UK, July 24-25, 2014 |

Published by Springer International Publishing

View Publication

Satisfiability modulo theories (SMT) solvers that support quantifier instantiations via matching triggers can be programmed to give practical support for user-defined theories. Care must be taken to avoid so-called matching loops, which may prevent termination of the solver. By design, such avoidance limits the extent to which the SMT solver is able to apply the definitions of user-defined functions. For some inputs to these functions, however, it is instead desirable to allow unadulterated use of the functions; in particular, if it is known that evaluation will terminate.

This paper describes the program verifier Dafny’s SMT encoding of recursive user-defined functions. It then describes a novel encoding that, drawing on ideas from offline partial evaluation systems, lets the SMT solver evaluate “safe” function applications while guarding against matching loops for others.