Hichem R. A.

I don't know if it is an infinite loop. It seems to me that when it instantiates the quantified formulas, it generates terms that contain high degree polynomials and the...

This PR needs to be merged otherwise all new PRs and PRs that have recent commits will keep having failing CIs

It actually failed in a **new** way. The error is not the same as the one it fixes. I created a PR #525 which should fix the new CI error

The migration was done in the PR #513.

@Stevendeo I'll mark this as a draft for now since I wanted to do the context reinitialisation more dynamically and avoid using literals for the integer ids.

This PR will have to wait for a new release of dolmen before being reviewed/merged as it uses its latest version

Suggestion (Inspired by what is done in https://git.frama-c.com/pub/colibrics): As it was done in the older version, tests can be kept in folders which separate them by their expected result (`../theory/{sat|unsat|unknown}/*.{ae|smt2}`)....

It's done.

LGTM, although I'm not sure about the deletion of the `challenges`, `incorrect` and `gui` tests. `incorrect` and `gui` don't seem very useful (at least not as non-regression tests, if someone...

Since they are in the `valid` folder it's probably safe to assume that they are valid. Looking at a few of them: - https://github.com/OCamlPro/alt-ergo/blob/4c02677244ba610466d5068011ea4dd69fc91577/non-regression/challenges/valid/challenge-case-split-non-pred-booleans__KO.ae#L1-L8 - https://github.com/OCamlPro/alt-ergo/blob/4c02677244ba610466d5068011ea4dd69fc91577/non-regression/challenges/valid/testfile-arith_mult_interval005__KO.ae#L1-L3 - https://github.com/OCamlPro/alt-ergo/blob/4c02677244ba610466d5068011ea4dd69fc91577/non-regression/challenges/valid/challenge_with_rational_division__KO.ae#L1-L6 They are...