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

[Leonardo de Moura]

Hi Alberto,

> Both z3 1.2 and yices 1.0.12 report "sat" for them, while spear 2.3
> reports unsat for the first two, and times out (1 hour on our machines)
> for the third. According to our experiments, we get different results
> with different semantics of division by zero which, as far as we
> understand, should be undefined, meaning that it should be ok to choose
> whatever semantics is liked. Is our interpretation correct?
> We got it from this passage of
> http://goedel.cs.uiowa.edu/smtlib/theories/BitVectors.smt:
>   Note that the semantic interpretation above is underspecified because
>   it does not specify the meaning of (bvudiv s t) or (bvurem s t) in
>   case bv2nat([[t]]) is 0.  Since the semantics of SMT-LIB's underlying
>   logic associates *total* functions to function symbols, we then
>   consider as models of this theory *any* interpretation conforming to
>   the specifications above (and defining bvudiv and bvurem arbitrarily
>   when the second argument evaluates to 0).  Benchmarks using this
>   theory should only include a :status sat or :status unsat attribute
>   if the status is independent of the particular choice of model for
>   the theory.

I think this passage confuses more than clarifies the issue, and I was unaware of the last sentence.

I discussed this issue with several people (e.g., Nikolaj Bjorner, Domaboj Babic, Armin Biere, Levent Erkok).
I was assuming the semantics of division by zero in SMT-LIB was underspecified, and it was *not* ok to choose whatever semantics is liked.
That is, a formula F is unsatisfiable if there is no model M for it, consequently we have to consider all possible interpretations for division by 0.
In other words, division by 0 is like an uninterpreted function.

In Z3, we implement (bvsdiv x y) using an auxiliary uninterpreted function bvsdiv0:

(ite (= y 0) (bvsdiv0 x) (fixed-bvsdiv x y))

Where fixed-bvsdiv uses a particular interpretation for division by 0. In our case, it is whatever the circuit, we use during bit-blasting, produces.

When we discussed this issue with Armin Biere, he had a good argument against this interpretation.
His main point is that the result of dividing by zero should be the output produced by real divider circuits in hardware systems.
That is, the largest unsigned integer that can be represented with the bit-width of the operands.
Moreover, if someone wants the underspecified semantics, he/she can just replace every occurrence of (bvsdiv x y) with the if-then-else term above.

I also believe it is simpler to implement the division operators with a fixed interpretation (i.e., the one used in hardware systems).
Some solvers in the QF_BV do not support uninterpreted functions, so the trick described above would not be straightforward to implement.

> If our interpretation is correct, then maybe such instances should not
> be part of the competition pool?

I'm also very curious about that.

Cheers,
Leo