[SMT-LIB] [SMT-COMP] Draft of SMT-LIB 2.5: request for feedback

[Delcypher]

Hi Florian,


> Dear SMTLIB community,
>
> as a member of the sonolar team I must say that our solver's output
>
> (((select a #b00000001) #b00101010)
> ((select a #b00000010) #b00000001))
>
> in response to
>
> (declare-fun a () (Array (_ BitVec 8) (_ BitVec 8)))
> (assert (= (_ bv1 8) (select a (_ bv2 8))))
> (assert (= (_ bv42 8) (select a (_ bv1 8))))
> (check-sat)
> (get-value (a))
>
> is not strictly correct wrt. the standard, since the sort of the returned
> value must be the same as the sort of the corresponding term in the
> get-value command.
> We simply found it easier to use and implement than introducing new
> auxiliary functions.

Thanks for the information. When I was looking at this a few years ago
I actually found SONOLAR's output much more useful than Z3's.

```
((unnamed_1 (_ as-array k!0)))
```

doesn't tell me anything useful were as your output actual told me
what I wanted to know

What I did in the was call (get-value) of every single array element
(in the problem I was tackling at the time I was using SMT-LIB arrays
to model arrays of finite length) which can be very expensive if the
array is large.

```
(get-value ( (select unnamed_1 (_ bv0 32) ) ) )
(get-value ( (select unnamed_1 (_ bv1 32) ) ) )
(get-value ( (select unnamed_1 (_ bv2 32) ) ) )
(get-value ( (select unnamed_1 (_ bv3 32) ) ) )
...
``

Thanks,
Dan.