[SMT-COMP] [SMT-LIB] SMT-COMP 2016: Draft Rules and Timeline Available

[François Bobot]

Hi,

On 17/05/2016 04:43, Dejan Jovanović wrote:
>  Also, we'd like to encourage people to do develop new
> solvers and participate, and addition of UF can be quite a burden if the
> solver doesn't already support it.
>
> Does anyone else have an opinion on this?
>

If the partial functions are totalized using a fixed arbitrary value, the users of the tools need to 
use UF symbols in order to use it reliably. So in that case the problems send to the provers in 
production will be QF_UFBV.

So could we just move the totalized partial function from the logic QF_BV to QF_UFBV, same for 
QF_NIA to QF_UFNIA and keep the current no-surprise semantic? That will give a barrier of entry for 
QF_BV low and keep the current theory.

-- 
François