Re: [Smtcomp-discussion] benchmarks involving divide by zero

[Tjark W. <tja...@it...>]

Florian,

On Thu, 2014-06-12 at 14:04 +0200, Florian Lapschies wrote:
> Am I right to assume that the desired behavior is to allow all values in 
> the case of division by zero while ensuring that all instantiations of 
> bvudiv behave the same?

(bvudiv s #b0) simply denotes an unknown value. Any interpretation is
permitted, i.e., is a satisfying model (if there are no other
constraints in the benchmark). Note that (bvudiv t #b0) may denote a
different value if s <> t.

Perhaps the note at the end of
http://smtlib.cs.uiowa.edu/theories/FixedSizeBitVectors.smt2
explains this more clearly.

> If yes, does this value have to be the same across all bitwidths?

I believe there is no such constraint.

Best,
Tjark

[Disclaimer: These comments are my own interpretation of the SMT-LIB
standard and have not been coordinated with the other members of the
SMT-COMP organizing committee.]