100x performance degradation when switching from 4.8.15. to 4.12.2 version

[PinkFrojdSenjak]

With the only change being z3-solver version, time for computing the solutions of problem increased 100x. The logic used is QF-NIA logic. The solver used is default (no explicit tactic calls).

[NikolajBjorner]

set smt.arith.solver=2 for your use. You can supply regression benchmarks. We are already working through known regression benchmarks and are currently updating z3. Updates to NIA specific parts are still in experimental branches.