On Satisfiability Modulo Computable Functions EPFL-REPORT-161285

Abstract. We present a semi-decision procedure for checking satisfia-bility of formulas in the language of algebraic data types and integer linear arithmetic extended with user-defined terminating recursive func-tions. Our procedure is designed to integrate into a DPLL(T) solver loop, using blocking clauses to control function definition unfolding. The proce-dure can check the faithfulness of candidate counterexamples using code execution. It is sound for proofs and counterexamples. Moreover, it is ter-minating and thus complete for many important classes of specifications: for satisfiable specifications, for specifications whose recursive functions are sufficiently surjective, and for functions annotated with inductive postconditions. We have implemented our system in Scala, building on top of the Z3 API and Z3’s plugin mechanism. Our results show our ap-proach to be superior in practice to the alternative of encoding recursive functions as quantified axioms. Using our system, we verified detailed correctness properties for functional data structure implementations, as well as Scala syntax tree manipulations. We have found our system to be fast for both finding counterexamples and finding proofs for inductively annotated specifications. Furthermore, it can quickly enumerate many test cases satisfying a given functional precondition, which can then be used to test both functional and imperative code. Thanks to our tool, many SMT solver clients, including verifiers and synthesizers, can ben-efit from the expressive power of recursive function definitions within formulas.