Loading preludes after statements that must be processed in start mode

[Halbaroth]

The preludes are loaded at the very beginning of the file. For instance, consider the file

<--- preludes here
(set-option :sat-solver tableaux)
(set-logic ALL)
(declare-const x Int)
(assert (= x 0))
(check-sat)

dune exec -- alt-ergo test.smt2 gives

(error "test.smt2:1.0:
error setting ':sat-solver', option value cannot be modified after initialization")

It makes sense because the preludes have been loaded using the default SAT solver, so we cannot switch the SAT solver after loading preludes.
There are actually three bugs:

1. We do not change the state to assert after asserting axiom. So the following file

<-- preludes here
(set-logic ALL)
...

is accepted even if the set-logic statement must be processed in start mode.
2. We do not reload the preludes after reset.
3. We do not process start mode statements before loading the preludes.

All the bugs are triggered in #1288.

A simple solution consists in processing start mode statements first at the begin of the file and after each reset statements. For instance:

(set-option :sat-solver tableaux)
(set-logic ALL)
....
(reset)
(set-option :sat-solver cdcl)
....

must be translated into

(set-option :sat-solver tableaux)
(set-logic ALL)
<--- preludes 
...
(reset)
(set-option :sat-solver cdcl)
<-- preludes
...

[bclement-ocp]

Ah, that's a good point. I guess that more specifically we should process preludes immediately after the start -> assert transition — I don't remember if we have a mechanism to do things on a specific transition though.