[SMT-LIB] Counterexample generation in Autoactive Verification using SMT

[Claude Marché]

Dear SMT-LIB list,

In the future work section of the following paper that was recently
published in the proceedings of SEFM'2016 :

  http://link.springer.com/chapter/10.1007/978-3-319-41591-8_15

some issues are raised:

1) lack of standard in SMT-LIB for displaying values in models found,
especially regarding array values, and values of non-interpreted types

Is there any progress in this direction ?

2) need for good candidate models even in presence of undecidable
theories (quantifiers, resp. NIA) that should at least satisfy the
ground part, resp. the linear part, of the input.

Such a question was discussed during a Dagstuhl seminar in October 2015,
and a little discussion followed on the CVC mail list:
http://cs.nyu.edu/pipermail/cvc-users/2015/000710.html

Any indeed on how this could be achieved? Soft/hard time limits as
suggested by the paper? Any idea on achieving this using the current
implementations of SMT solvers?

Thanks in advance for any feedback,

- Claude

-- 
Claude Marché                          | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |