Handling decisions in SMT-LIB

[Tomáš Kolárik]

Dear SMT-LIB community,

I would like to draw your attention to the discussion on handling
decisions of SMT solvers in the standard.
I drafted a proposal of several commands on the topic in the following
thread on the official SMT-LIB GitHub:

https://github.com/SMT-LIB/SMT-LIB-2/discussions/35

I invite you to join the effort to gather a group of interested people
and to collect feedback.
I also plan to write the proposal as a submission to the SMT workshop.
We already identified several use-cases of the overall idea (@Clark
Barret, @Alberto Griggio).

There is a family of satisfiable incremental benchmarks in the SMT-LIB
that remains unsolved:

https://smt-comp.github.io/2024/results/qf_bvlra-incremental/

.. because the original benchmarks rely on guiding the decisions.

Best,
Tomáš Kolárik
Maintainer of OpenSMT