[SMT-LIB] QF_BV and division by zero

[Viktor Kuncak]

Dear Tjark,

Neither myself nor most people in my group (with some notable exceptions!)
are SMT solver developers, yet I still favor this proposal to change to
more interpreted semantics, so it is not for implementation reasons.

Uninterpreted semantics gives only an illusion that one can use simple
modeling. Many formal methods applications will have non-deterministic
behavior for errors, so deterministic uninterpreted functions are making
the problem more subtle instead of solving it. In languages with checked
exceptions we need to take care of things like

 try { 1 / 0 } catch { case _ => 42 }

so uninterpreted functions are of no help there either.

So, if the proposed change means that now more people will realize that
they need to explicitly model behaviors where the source system gives an
error, that, in my view, will be a good thing.

Best regards
  Viktor

On Thu, Oct 15, 2015 at 1:31 PM Tjark Weber <tjark.weber at it.uu.se> wrote:

> On Wed, 2015-10-14 at 22:08 -0700, Clark Barrett wrote:
> > So, we are proposing to change the semantics of bit-vector division so
> > that division by zero produces a vector of all 1's.
>
> I still believe that this is not a very good idea. Already today, one
> of the most common problems in the application of formal methods is
> that users do not model their systems correctly.
>
> The proposed change makes life slightly easier for solver developers,
> but it shifts the burden to the users of bit-vector logics. Users will
> need to be aware that it is no longer sound to simply use 'bvdiv' to
> model bit-vector division, *unless* the system that they are modeling
> happens to guarantee that the result of division by 0 is all 1's.
>
> I am guessing it won't be very long until someone uses 'bvdiv' in an
> unsound manner because they were not aware of this subtlety.
>
> However, it appears that you've already weighed this argument. I do
> welcome that this semantic issue is being resolved at last. Any clear
> resolution is an improvement over the current situation, and hopefully
> will allow us to include benchmarks that use bit-vector division in the
> SMT Competition again next year.
>
> Best,
> Tjark
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>