[SMT-LIB] minor updates to benchmarks

Domagoj Babic babic.domagoj at gmail.com
Mon Jun 18 16:13:30 EDT 2007


Hi Clark,

My parser says something's wrong (supposedly, AND or BVAND has only one
parameter) in QF_BV benchmark testcase15.stp.smt : 717394.

However, since that particular line has 20.222.495 characters (!), I
couldn't find
exactly the column where the problem starts.

BTW, this nesting style of dumping formulas is _really_ inconvenient for
debugging. Would it be possible to flatten the benchmarks in the future
(like in Spear format)?

On 6/18/07, Clark Barrett <barrett at cs.nyu.edu> wrote:
> Also, the QF_BV tar file seems to have been missing some benchmarks.  Also, the
> status and difficulty for the tacas07 benchmarks was unknown.  These have been
> updated and the tar file now contains all the updated benchmarks.

Regards,

-- 
        Domagoj Babic

        http://www.domagoj.info/


More information about the SMT-LIB mailing list