[SMT-LIB] bitvector benchmarks with division

[Clark Barrett]

I'd like to update the community on our effort to screen benchmarks containing
bitvector division (and similar operators) for the SMT competition.  As you may
recall, last year, we eliminated all benchmarks containing any division,
modulo, or remainder operations because different solvers were getting
different answers.

The reason for this is that different solvers interpreted division by zero
differently.  According to the SMT-LIB definition of the bitvector theory, a
formula is unsatisfiable only if it is unsatisfiable *regardless* of how
division by zero is interpreted.  Last year, we had no way to determine this.

This year, we have better news.  We were able to generate type-correctness
conditions for all bit-vector benchmarks.  These are formulas that have the
following property: if the TCC is unsatisfiable, then the evaluation of the
original formula does not depend on the interpretation of division by zero.  We
checked TCC's using three bitvector solvers: CVC3, z3, and boolector.  All
agreed on the results.

In QF_BV, there are 6015 benchmarks containing one of the problematic
operators.  Of these, 4554 were proved unsatisfiable, meaning they can safely
be used in the competition.  1461 were satisfiable meaning that they may be
unsafe.  We plan to remove these benchmarks from consideration during the
benchmark selection phase.

In QF_AUFBV, only 12 benchmarks contain a problematic operator.  5 of them have
unsatisfiable TCC's.  The other 7 are satisfiable and will be removed from
consideration.

The complete list of benchmarks with satisfiable TCCs is attached.  These
benchmarks will not be used in SMT-COMP 2009.  However, any bitvector benchmark
*not* in the list may be selected.

-Clark
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: tcc_sat.txt
Url: /pipermail/smt-lib/attachments/20090724/9f822ea2/tcc_sat-0001.txt