search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
368 stars 46 forks source link

smtlib-model-format default for yices-smt2 #411

Closed ahmed-irfan closed 1 year ago

ahmed-irfan commented 1 year ago

This PR makes the smtlib-model-format model printing option default for the yices-smt2.

Updates to: Code + tests + manual

disteph commented 1 year ago

@BrunoDutertre: This was one of the requests in #402: yices-smt2 takes SMTLib2 in, it makes sense to make it give SMTLib2 out. It is, however, breaking backward compatibility for scripts that parse the models output by yices-smt2. Breaking backward compatibility means it should get into Yices 2.7, correct? I'm OK making master target 2.7 already; if we need bug fixes to 2.6.4 we can have a dedicated branch. Objections?

BrunoDutertre commented 1 year ago

No objections from me. It makes sense to increase the version number.