Tags:MCSat, SMT, Theory of Arrays and Weakly Equivalent Arrays
Abstract:
In this paper, we present the support for the (extensional) theory of arrays in the MCSat scheme for SMT solving. We describe its implementation in the (MCSat component of) the Yices2 SMT-solver, allowing Yices2 to solve, for the first time, benchmarks that combine arrays with non-linear arithmetic. Our experimental results show that this implementation outperforms other state-of-the-art SMT solvers when solving such benchmarks (QF-ANIA + QF-AUFNIA), and also demonstrates decent performance on other SMT logics that involve arrays.