Incremental Linearization For Satisfiability And Verification Modulo Nonlinear Arithmetic And Transcendental Functions

The tarball contains Satisfiability Modulo Theories (SMT) and Verification Modulo Theories (VMT) benchmarks for the theories of Nonlinear Real Arithmetic (NRA) and NRA extended with Transcendental Functions (NTA). These benchmarks have been collected in the following works: Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. "Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF". In proc. Tools and Algorithms for the Construction and Analysis of Systems, TACAS'17, 2017. Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. "Satisfiability Modulo Transcendental Functions via Incremental Linearization". In proc. Int. Conference on Automated Deduction, CADE, 2017. Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. "Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions". ACM Transactions on Computational Logics. 2018. To appear.