[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