SIGSEGV in loop acceleration with z3

[SaswatPadhi]

CBMC version: develop
Operating system: Mac OS
Exact command line resulting in the issue: make in regression/acceleration with z3 installed
What behaviour did you expect: Regression tests to pass
What happened instead: 3 of the regression tests crash with segmentation fault

This was exposed in #5944.

When z3 is installed, the regression tests fail.
When z3 is not installed, the regression tests pass!

goto-instrument seems to silently ignore errors in running the SMT solver, and treats errors as an UNSAT result!

[SaswatPadhi]

I linked a PR that fixes the issue of solver errors being ignored, and changes the default solver from Z3 to CPROVER_SMT2.

But I am leaving this issue open because we should debug z3 issues with loop acceleration code at some point in the future.

[thomasspriggs]

This should be fixed in fa657ac

[thomasspriggs]

This has been fixed as part of #5944.