[SMT-LIB] R: smt-comp scrambler

[Alberto Griggio]

Hllo Christoph,

> I'm fairly certain that there is a bug in the scrambler published on the smt-comp 11 website:
> 
> I used -seed 1234 on file QF_BV\check2\symbols.smt2
> 
> In the function declarations of the output, all variables are renamed to x* but two of the original names (v1, |v0|) still appear in some of the > assertions.
> 
> Of course, it would be very much appreciated if this could be fixed before the competition :)

Thanks for the info! We are aware that there is a bug in the scrambler *for that specific benchmark*. The above benchmark is quite "nasty", as it tries to use several funny names that might confuse a non-strictly-conformant parser. It seems that the one used by the scrambler gets hit by this, unfortunately. 

I will fix the problem as soon as possible. However, we have decided to not include that specific benchmark in the competition, both because of this issue with the scrambler, and because once it gets scrambled, it becomes pointless (since its purpose is to test the conformance of the parser in the presence of weird symbol names). To the best of my knowledge, the rest of the benchmarks in the SMT-LIB do not expose that particular bug. However, I will double check ASAP.

Alberto