Evaluate sat.smt=true option for z3

[palinatolmach]

Related: Z3Prover/z3#7507

We have a test suite-produced script timeout-4.13.4.smt2.txt that times out with z3 v4.13.4 in the ite statement evaluation.
In the issue we opened in the z3 repository, sat.smt=true was recommended as a way to avoid this issue. Adding the option in haskell backend/booster by @jberthold caused the prover to loop and the = sign to be missing in the output.

The legacy backend does not use smtlib-backends-process (directly uses System.Process) and does not seem to have this problem.

• Investigate why the solver cannot be used by booster with the sat.smt=true option
• (We already have a CLI option to pass options to the SMT solver). Test what happens when passing the option via CLI.
• Once the solver can be started and used with this option: Evaluate performance impact of the option. @PetarMax mentioned that this sat.smt=true option used to slow down Z3 operations.