New divisions in the Model-Validation Track

[BOBOT Francois]

Hello!

we want to try out some new, experimental divisions in the

Model-Validation Track of future SMT Competitions; if possible even one

or two already this year. Candidates for new divisions are

QF_NonLinearIntArith (QF_NIA, QF_NIRA), QF_NonLinearRealArith (QF_NRA),

QF_Datatypes (QF_DT, QF_UFDT), and QF_Array (QF_AX). This means we need

to define acceptable formats for models in these divisions. Please send

us your preferred model formats for the associated logics and existing

model formats if you already have a solver that returns a model for one

of the associated logics. Of particular interest to us are answers to

the following questions:

How do you (want us to) represent the value of an array constant?

How do you (want us to) represent irrational algebraic numbers as

values

of constants?

How do you (want us to) represent the undefined part of the projection

function in datatypes?

At the same time clarification for how to represent the model for

division by zero is welcomed.

Sincerely,

The SMT-COMP organizing team

François Bobot (chair), CEA List, France

Martin Bromberger, MPI for Informatics, Germany

Jochen Hoenicke, Certora, Israel