smtlib2 tests with multiple solvers use z3 almost always

[gustavo-grieco]

Most of the smtlib2 tests have the use of the z3 solver hardcoded:

https://github.com/trailofbits/manticore/blob/fd83be7a9929d3645a3df995e2f925d3fb3b4b7f/tests/other/test_smtlibv2.py#L995-L1020

Instead, they should use self.solver since that variable is properly initialized to have the correct instance:

https://github.com/trailofbits/manticore/blob/fd83be7a9929d3645a3df995e2f925d3fb3b4b7f/tests/other/test_smtlibv2.py#L1283-L1295

A fix for this is coming in #2420