[SMT-LIB] QF_BV and division by zero

[François Bobot]

Le 30/03/2017 à 05:52, Trevor Hansen a écrit :
> It'd be great to have QF_BV division and remainder by zero resolved in time for this year's SMTCOMP.
> The relevant discussion from 2015 is in the thread here:http://www.cs.nyu.edu/pipermail/smt-lib/2015/000966.html

The original choice of the SMTLIB is to totalize partial function by accepting all interpretations 
instead of fixing one. I understand it as a choice of least surprise for the user. I acknowledge 
that in some cases it complicates the work or the efficiency of the solvers.


But for my part I prefer to be sure of what I'm proving, so I prefer the current choice and I'm 
worried that adding exceptions to the rule lead to removing the rule.

Why QF_BV division and remainder should be different from any other partial function? Does your 
argument should not apply to any SMTLIB partial function?


Best,

-- 
François Bobot