[SMT-COMP] Some further questions on benchmarks status and difficulty

[Armin Biere]

On Fri, Jun 6, 2008 at 6:02 PM, Leonardo de Moura
<leonardo at microsoft.com> wrote:
>> If our interpretation is correct, then maybe such instances should not
>> be part of the competition pool?
>
> I'm also very curious about that.

In addition I think it is really hard (probably needs quantifiers over
uninterpreted functions)
to check that definedness of a formula does not depend on the specific
interpretation of x/0.

Just for completness:   Here is an axiom, I would suggest to add to QF_BV:

(benchmark udivzero
 :logic QF_BV
 :extrafuns ((s BitVec[32]))
 :formula (not (= (bvudiv s bv0[32]) (bvnot bv0[32]))))

which means unsigned division gives UINT_MAX.

In case we keep the axioms on 'smtlib' for 'sdiv' this implies
that a positive number divided by zero is also UINT_MAX, which
is -1 interpreted in two-complement and a negative number
will result in 1:

(benchmark negsdivzero
 :logic QF_BV
 :extrafuns ((s BitVec[4]))
 :assumption (bvslt s bv0[4])
 :formula (not (= (bvsdiv s bv0[4]) bv1[4])))
(benchmark possdivzero
 :logic QF_BV
 :extrafuns ((s BitVec[4]))
 :assumption (bvsge s bv0[4])
 :formula (not (= (bvsdiv s bv0[4]) (bvnot bv0[4]))))

I would prefer INT_MAX and INT_MIN respectively, but I am not sure that
this makes sense.

Armin