SMTlib 2 Benchmarks for MCSat-based Finite Field Reasoning in the Yices2 SMT Solver. Requires Yices2 compiled with finite field support: Ovascos/yices2
Benchmarks are taken from:
- Hader, T., Kaufmann, D., Kovács, L.: SMT solving over finite field arithmetic. In: Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). EPiC Series in Computing, vol. 94, pp. 238–256. EasyChair (2023)
- Ozdemir, A., Kremer, G., Tinelli, C., Barrett, C.W.: Satisfiability modulo finite fields. In: Intl. Conf. on Computer Aided Verification (CAV), Part II. LNCS, vol. 13965, pp. 163–186. Springer (2023)