[SMTCOMP] scrambler

Leonardo de Moura demoura at csl.sri.com
Wed Aug 9 13:11:47 EDT 2006


Hi,

We made a minor modification in the scrambler. This modification
only affects how variables are declared. It doesn't affect the formula
or the order the variables appear in the problem. We made this
modification because one of the submitted solvers did not support
declarations such as:

    :extrafuns ((x1 Int) (x2 Int))

So, the new scrambler generates

    :extrafuns ((x1 Int))
    :extrafuns ((x2 Int))

This solver would score 0 in all divisions without this modification.
We would rather have this solver in the competition than out because  
of a
technicality like this.

BTW, this solver was *not* submitted by the organizers.

Best wishes,
Leonardo for Aaron and Clark too.




More information about the SMT-COMP mailing list