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

[Alberto Griggio]

Hi all,

first, thanks a lot for your work on the new standard! This said :-),
here's my feedback:

- I agree about letting the user call get-model and/or get-value after a
   check-sat-assuming. That is an essential feature IMHO.

- For simplicity, I'd keep the check-sat-assuming command instead of
   having an extra "assume" command that modifies the assertion stack

- I think that check-sat-assuming should also allow to have negated
   Boolean constants as input, not just "plain" Boolean constants. I.e it
   should be possible to have something like:

        (check-sat-assuming (v1 v2 v3 trans (not init) (not bad)))

- I think (reset-assertions) should not remove declarations if
   :global-declarations is true. The way I see it, setting
   :global-declarations to true means that declarations are not part of
   the assertion stack at all, so resetting the latter should have no
   impact on the former.

- the draft says that the echo command prints back the string *including
   the double quotes*. Is there a specific reason for this? It sounds
   strange to me (and it is not they way current solvers supporting echo
   work -- at not for Yices2, MathSAT and Z3)

- I agree about not deprecating set-info, for the reason given by Morgan


Alberto