Starting missing timer

[Stevendeo]

The Options.Timer was not started at the beginning of alt-ergo. This led to a very strange behavior:

$time dune exec -- alt-ergo --timelimit=1 --enable-assertions --output=smtlib2 --sat-solver CDCL tests/everything/f1.ae 

; File "tests/everything/f1.ae", line 159, characters 1-166: Valid (1.6413) (13477 steps) (goal WP_create)
;

real 0m1,804s
user 0m1,654s
sys 0m0,138s

As you can see, the goal is verified after 1.6413 even though we set a timelimit at 1. This is because alt-ergo's time corresponds (more or less) to the user time of the whole process with dune exec. If we remove dune exec -- and execute directly the binary, we get more consistent results :

$./alt-ergo --timelimit=1 --enable-assertions --output=smtlib2 --frontend dolmen --sat-solver CDCL tests/everything/f1.ae 
alt-ergo: option '--frontend': this option is deprecated and will be ignored in the next version

; File "tests/everything/f1.ae", line 159, characters 1-166: Valid (0.6038) (13477 steps) (goal WP_create)
; 

If we set the timer (as it is done for the legacy loop), we get consistent results.

[Stevendeo]

Also, because of some Flying Spaghetti Monster kerfuffle, it makes a test pass on my laptop that started failing few days ago (and that made the CI of next fail for 5.0.0 on mac)

EDIT: nevermind, the problem is still here.

[Halbaroth]

I cannot reproduce the other bug on my laptop. We should open an issue about it.

[bclement-ocp]

Ah I had noticed inconsistencies with timers when using Dolmen, so that's what it was. Thanks for the fix!

[bclement-ocp]

Also, because of some Flying Spaghetti Monster kerfuffle, it makes a test pass on my laptop that started failing few days ago (and that made the CI of next fail for 5.0.0 on mac)

EDIT: nevermind, the problem is still here.

Yeah there are some tests that are juuuust solved in the timelimit we use for tests and cause spurious failures. We should collect those and increase (double?) the timeout for those.