[SMTCOMP] a question on the benchmark scrambler

[Hyondeuk.Kim@colorado.edu]

Hi Leonardo,

I wonder how equalities can be permuted.

Thank you.

Hyondeuk

Quoting Leonardo de Moura <demoura at csl.sri.com>:

> 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
>