benchmarks with integer arithmetic and exponentiation

[ffrohn]

Benchmarks generated by the verification tool LoAT to evaluate the SMT solver
SwInE. We extracted all benchmarks with exponentiation that were generated by
LoAT when analyzing the examples from the category LIA-Lin (linear CHCs with
linear integer arithmetic) of the CHC competitions 2022 and 2023, and when
analyzing the examples from the categories "Termination of Integer Transition
Systems" and "Complexity of Integer Transition Systems" of the Termination and
Complexity Competition 2024. From the entire set, we selected those where

• SwInE v0.1.0 or SwInE-Z3 v0.1.2 failed or needed more than 1 second, or
• SwInE-Z3 v0.1.2 failed without phasing, a technique to prevent SwInE from
  computing with huge constants (described here
  https://arxiv.org/abs/2502.04761)
  If several selected benchmarks only differed in lines not containing
  exponentiation, we kept only one of them.