[SMT-COMP] 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