Retry SMT queries in Booster when deciding predicates

[geo2a]

Fixes #3884

• refactor the SMT modules to allow re-initializing the solver dynamically:

  • SMTContext now carries the prelude and SMTOptions
  • the closeContext function only closes the solver handle, and does not close the solver transcript handle. The new destroyContext function does both.
  • The SMT monad is is changed to have StateT SMTContext. The Booster.SMT.Interface.restartSolver function restarts the solver with modified options, altering the context. Note that it does not touch the transcript handle, i.e. it will persist the sovler restarts.

• the getModelFor and checkPredicates functions now have logic to retry with doubled timeout when the solver returns unknown.

I'm checking-in the integration test that I was using when developing. I ran the server with --smt-timeout 1 to observe the retry mechanism kicking-in, but I do not think it is a good idea to try to force it to retry the queries in CI. The test may still be useful when working on the SMT code in future.

[geo2a]

No difference in KEVM performance:

Test	georgy-retry-smt-in-booster time	master-7f482b016 time	(georgy-retry-smt-in-booster/master-7f482b016) time
benchmarks/storagevar00-spec.k	50.06	51.85	0.9654773384763742
mcd/dai-symbol-pass-spec.k	57.66	59.72	0.965505693235097
benchmarks/storagevar01-spec.k	51.36	49.32	1.0413625304136254
TOTAL	159.07999999999998	160.89	0.9887500776928336

[geo2a]

The test-log-simplify-json integration test failure has been solved by e867eed --- we should wait until the server is stopped before we compare the log file to the golden one.

[goodlyrottenapple]

Looks great! Left some minor comments