[SMT-COMP] StarExec Test Jobs Started

[BOBOT Francois]

Dear Solver Authors,

We have done a third test run for the model validation track, since
the second one was missing some updated solver, and a fixed script for dolmen
 ("--strict=false" is now used instead of "--force-smtlib2-logic=ALL").

https://www.starexec.org/starexec/secure/details/job.jsp?id=59315

[The deadline for final solver version is extended until monday 29 May AOE]


However the results of the second run with the fixed script are available at
https://drive.google.com/file/d/1PPaVr9-VXbEpet0SqFjaZk6egxnKEKF4/view?usp=share_link

for reference the input problems used and model computed by the solvers are available at:
https://drive.google.com/file/d/10-O18Gbsvo_ABaezo0h3G0OOpp0eU5M6/view?usp=share_link

Since the result are quite big, follows some remarkable points of concern:


## SMT-RAT-MCSAT

I'm sorry that the first proposed syntax for algebraic datatype was not using
correct SMTLIB terms:

(root-of-with-interval (p_0 p_1 ... p_n) (min max))

it is now using:

(root-of-with-interval (coeffs p_0 p_1 ... p_n) min max)

SMT-RAT-MCSAT still uses the old one

## CVC5

CVC5 uses its own algebraic number syntax which is not an SMTLIB terms, which makes it hard to parse

```
(define-fun x1 () Real (_ real_algebraic_number <1*x^2 + 4*x + (-4), (3/4, 1)>))
```

## YICES

Yices as an unsoundness, CVC5 agree with dolmen:
```
=================================
output/track_model_validation/QF_UFNRA/20230328-sqrtmodinv-hoenicke/Yices 2 model valid
ation for SMTCOMP 2023___default/sqrtStepFinal.smt2/input.rsmt2
there is a sat
File "tmp/tmp.sezfAIWBef.smt2", line 23, character 0-41:
23 | (assert (= (- (/ x6 x9) (x2 x6 x9)) x11))
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error This hypothesis/assertion evaluates to false
```

It suffer of some segmentation fault

```
output/track_model_validation/QF_AUFNIA/UltimateAutomizer/Yices 2 model validation for SMTCOMP 2023___default/s3_clnt.blast.01_false-unreach-call.i.cil.c_0.smt2/input.rsmt2
there is a sat
File "tmp/tmp.nFMoSazNDY.rsmt2", line 2, character 1-57:
2 | /export/starexec/sandbox/solver/bin/starexec_run_default: line 3: 56051 Segmentation fault (core dumped) ./yices2 $1
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error Syntax error (state 172) while reading the symbol '/export/starex…'.
```

* Uses a function for giving the model of an array, which can be an interesting propasal but not yet implemented.

```
=================================
output/track_model_validation/QF_ABV/egt/Yices 2 model validation for SMTCOMP 2023___default/egt-7791.smt2/input.rsmt2
there is a sat
File "tmp/tmp.PXbSD8uO95.rsmt2", line 3, character 3 to line 14, character 146:
3 | ...(define-fun
4 | x1
...
13 | (ite (= x!0 #b00000000000000000000000101110010) #b00110010
14 | (ite (= x!0 #b00000000000000000000000011110000) #b00110101 (ite (= x!0 #b00000000000000000000000011110010) #b00000001 #b10000000)))))).
Error Incoherent redefinition for term constant `x1`.
The new definition has type:
Bitv_32 -> Bitv_8
but the declaration had type:
array(Bitv_32, Bitv_8)
`x1` was declared at line 3, character 0-54
=================================
```

## NRA-LS

NRA-LS seems to print sat but not the model:

output/track_model_validation/QF_NRA/20211101-Geogebra/NRA-LS-2023___default/IsoRightTriangle-Bottema1_3b.smt2/input.rsmt2



## z3++

For this year dolmen now accepts the syntax "-4" for coefficient, it would be better if it could be fixed in the solver.

```
=================================
output/track_model_validation/QF_NRA/20211101-Geogebra/z3++_mv_0522___default/IsoRightTriangle-Bottema1_3b.smt2/input.rsmt2
there is a sat
File "tmp/tmp.rrCoOohuwS.rsmt2", line 4, character 36-38:
4 | (root-of-with-ordering (coeffs -4 4 1) 1))
^^
Error Non-linear expressions are forbidden by the logic.
Hint: An integer constant is expected
```

## OpenSMT

Is OpenSMT participating in a category it doesn't support?

```
=================================
output/track_model_validation/QF_UFIDL/20210312-Bouvier/OpenSMT___default/vlsat3_l69.smt2/input.rsmt2
there is a sat
File "tmp/tmp.7Y79Y886If.rsmt2", line 1, character 1-2:
1 | (error "unknown logic QF_UFIDL")
^
Error while parsing an input statement, read an opening parenthesis,
but expected an opening parenthesis to start a command.
```

Best,

--
François