Satisfiability Modulo Extensional Constant Arrays (Extended Version)

TL;DR

This paper introduces a new decision procedure for the SMT theory of arrays with constant arrays, supporting arbitrary index domains and improving efficiency in verification tasks.

Contribution

It presents a novel calculus and implementation for array reasoning in SMT solvers, extending support to finite index domains with constant arrays.

Findings

Implemented in Bitwuzla SMT solver

Evaluated on diverse benchmarks

Supports arbitrary index domains

Abstract

Reasoning about array data structures is a key requirement for many applications in hardware and software verification, especially in combination with machine integers. The Satisfiability Modulo Theories (SMT) theory of extensional arrays provides array read and write operators and allows extensionality over arrays. This is sufficient to express many aspects of computer-aided verification, but lacks succinctness to efficiently deal with arrays that are initialized with a default value. Existing procedures for extending the SMT-LIB theory of arrays with support for constant arrays are limited to arrays with infinite index domains, and existing implementations in SMT solvers only support a fragment of the theory for finite index domains. In this paper, we present a novel decision procedure for the theory of arrays with constant arrays that supports arbitrary index domains and is not limited to the infinite case. We present our procedure as an abstract calculus and show its refutational and satisfiability soundness. We implement a decision procedure based on our calculus in the state-of-the-art SMT solver Bitwuzla and evaluate its performance on a diverse collection of benchmarks and use cases.