ibexsolve does not handle thick equalities as inequalities

[gchabert]

If inequalities are replaced by thick equalities, certification is disabled:
"warning: Certification not implemented for over-constrained systems"

[jermann-c]

Moreover, the writing of the MNF output file (v2) in this case seem to produce an extraordinary amount of data (file size in Gb for a not so gigantic number of solution boxes, e.g., less than 100k).

[gchabert]

Fixed but the "in" keword has to be used. The '=' symbol is interpreted as a parametric solving.
Ex:

x^2+y^2 in [0,1]

means that you are looking for the set of all solutions of f(x,y)=a when a is in [0,1].

[gchabert]

Example to explain the difference between. If one writes
x-y = [0,1]
Then the box [0,1]x[0,2] is an inner box since
for all a in [0,1] for all x in [0,1] exists y in [0,2] such that x = y + a

If instead one writes
x-y in [0,1]
then the box [0,1]x[0,2] is not inner. The box [0,0.5]x[0.5,1] is inner since
for all x in [0,0.5] for all y in [0.5,1], 0 <= x -y <= 1

Further, if you write more than two equalities f(x,y) = [...,...] then the solver disable proofs as the problem is considered as over-constrained.

[jermann-c]

Understood, thanks Gilles !