Re: [Smtcomp-discussion] benchmarks involving divide by zero
Tools and documentation of the annual SMT competition
Brought to you by:
webertj
From: Tjark W. <tja...@it...> - 2014-06-12 20:42:21
|
On Thu, 2014-06-12 at 09:03 -0700, Clark Barrett wrote: > As for changing the standard, I suggest this be brought up at the SMT > workshop during the SMT-LIB discussion. As there seems to be some > consensus, this will make a strong case for change. The discussion so far was very much from a solver developer's point of view. The user perspective is a bit different. In application contexts, bit-vector division by 0 may have undefined results. The current semantics is the closest we can come to modeling this in the total logic of SMT-LIB. Defining, e.g., bv_div x x00 = xFF turns this equation into an assumption that the application context must satisfy. Otherwise, any unsatisfiability result (e.g., any SMT-based verification of some algorithm) may be unsound. If even solver developers are sometimes not aware of the precise semantics of bit-vector division (as this thread has shown), we should not expect most users of SMT solvers to be aware of such an assumption. Thus, for every solver developer whose life would be easier with such an assumption, there will be n users who are unaware that they are building unsound models. This will cause pain (rejected papers, crashing rockets, ...) sooner or later. Just my two cents. Best, Tjark |