Halmos fails to start a different solver than Z3

[aviggiano]

Describe the bug

Trying to work around #402 by using yices, I still see the same error. This Z3 parser issue is unexpected, since I am explicitly using another solver.

To Reproduce

git clone https://github.com/aviggiano/halmos-modexp
cd halmos-modexp
halmos --solver-command yices-smt2

Environment:

• OS: macOS
• Python version: Python 3.12.6
• Halmos and other dependency versions: halmos 0.2.1.dev16+g1502e46

Additional context

N/A

[karmacoma-eth]

your workaround was worth a try, but the error happens internally before it reaches the external solver. For context, even when relying on an external solver for the actual assertion solving, we still internally rely on the Z3 API to handle symbols and build expressions -- this is where this fails. Will fix the underlying #402 issue