[SMTCOMP] a question on the benchmark scrambler

[Leonardo de Moura]

Hi Alberto,

> Am I right or not?

Yes you are correct.

> And if I'm right, is there any particular reason why this is not  
> done? Not that
> I'm saying that this must (or should) be done, it is more a
> curiosity...

I didn't do that because in QF_RDL and QF_IDL the linear arithmetic
atoms should have a specific format:

- (op (- x y) c),
- (op (- x y) (~ c)),

where op is "=, <, <=, >=, >"

I didn't want to change this format in the output produced by the  
scrambler
because some tools may assume it.

Anyway, if nobody depends on this restriction I can modify the scrambler
to permute equalities.

Leonardo