[SMT-COMP] FW: smt-comp scrambler

Sat Jul 9 22:35:09 EDT 2011

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Christoph Wintersteiger
Sent: Saturday, July 09, 2011 6:55 PM
To: smt-lib (smt-lib at cs.nyu.edu)
Subject: [SMT-LIB] smt-comp scrambler

Hi there,

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

Cheers,
Christoph

_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/smt-lib