Proving arithmetic properties has many applications, ranging from classical use cases of computer algebra and functional analysis to more applied case studies from software analysis and verification. For example, program loops over numeric data structures naturally implement addition, multiplication and exponentiation operations. While automating reasoning about such arithmetic properties has already made significant progress in the domain of linear algebra, non-linear reasoning in the context of satisfiability and validity checking is sill at its infancy. Although this subfield of automated reasoning is still quite unexplored, there do exist SMT-solvers (satisfiability modulo theory) which are able to reason about such non-linear arithmetic properties. Whenever new proving techniques or improvements are discovered, a typical approach to evaluate their performance is to test them on challenges of varying difficulty and compare different metrics like runtime or quality of the result (e.g. length of the proof) with those of other solvers. For non-linear arithmetic over reals and over integers, a large dataset of such challenges already exists (e.g. SMT-Lib benchmarks). Although these benchmarks are well suited for performance tests, they are often complex and only theoretically readable by humans. Therefore, it usually becomes difficult to get to the real problem when a benchmark is not solved. In this thesis, we describe various ways to generate benchmarks where the complexitycan be adjusted in different ways. The benchmarks are not created from scratch but are based on challenges originally designed for loop invariant generators. For a wide range of loops, these invariants can be represented by polynomials over the variables occurring in the program, which makes them a perfect fit for our benchmarks. The benchmarks formulate a correctness claim for polynomial loop invariants in first-order logic. All the methods described in this thesis for generating such benchmarks are proven to be sound. That is, we show that the correctness claim is a valid formula if and only if the corresponding polynomial invariant is indeed an invariant of the considered loop. The already mentioned variation of the benchmark is then achieved by exploiting properties of polynomial invariants. Experiments on the generated benchmarks were then conducted, using the two state-of-the-art solvers Vampire and Z3. Based on the resultsof the experiments, we have investigated the impact of varying the complexity of the benchmarks. Additionally, we suggest further approaches and adaptions to the solver in an attempt to improve their performance