[SMT-LIB] QF_BV64 benchmarks available

[Domagoj Babic]

Hi all,

Calysto v1.3 benchmarks are now available on my webpage in the Spear
Format (SF).

I've also written an sf2smt translator, which is also available on my
webpage (under
Spear Tools).

I've picked over the benchmarks on which Spear took over 10 sec on my machine
with either structural abstraction or eager expansion. It took over a
week to run
Calysto in both modes on all the benchmarks. Eager expansion is terribly slow,
and on some benchmarks (Samba) I had to kill Calysto after a couple of days, but
still, there is a plenty of Samba benchmarks.


I'm not sure if anyone here has analyzed the influence of various
translators on both
the performance and correctness. To assure that the semantics have been
maintained, I also wrote an smt2sf tool, and checked:

Spear --sf test.sf  ==  sf2smt test.sf | smt2sf --stdin | Spear --sf-stdin

The testing is still running, but so far all the results match. I did notice
that the difference in runtimes is occasionally significant.


sf2smt translator uses the bv(s)rem operators, as recently agreed, instead of
the old bv(s)mod operators. The name of the logic is tentatively QF_BV[64], but
that can be easily changed if really needed. If the change is needed,
please let
me know, so that I can modify the entire tool chain.


Note: I've just noticed that Clarke sent an email about the new version of SMT
format. None of the changes seem drastic, so I hope I will be able to update
both sf2smt and smt2sf some time tonight (check the news on my website
to see if the new versions have been released). In the meantime I'd appreciate
it very much if someone could try the current versions of both tools and see if
any other changes of the output are needed, besides those required by
the new standard.


Good luck with the competition organization,

                                                 Domagoj Babic