| ||||
| ||||
![]() Title:Arrays Reasoning in MCSat Conference:SMT 2024 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. Arrays Reasoning in MCSat ![]() Arrays Reasoning in MCSat | ||||
Copyright © 2002 – 2025 EasyChair |