Compatibility issue with newer versions of Z3/SMTLib

[acieroid]

System info:

$ z3 -version
Z3 version 4.8.10 - 64 bit

Using the latest commit of scala-smtlib, models are not annotated with the model symbol anymore, for example a model return by the latest z3 is the following:

(
  (define-fun z () Int
    1)
  (define-fun y () Int
    1)
  (define-fun x () Int
    2)
)

While on older version, it was:

(model 
  (define-fun y () Int
    1)
  (define-fun x () Int
    2)
  (define-fun z () Int
    1)
)

No unit test is currently broken because they use hard-coded models. The fix is quite simple in essence: removing lines 130 to 133 of ParserCommandResponses is enough to get responses to parse again. This has to be mirrored in the printer too.

However, properly fixing it probably requires dealing with both the old and the new format.

[regb]

Thanks for reporting this. Unfortunately, I haven't been following development in smtlib in the last few years. But here are some of my thoughts.

Generally, I have tried to follow the official SMT-LIB standard (http://smtlib.cs.uiowa.edu/language.shtml) for how to implement the parsers. If the standard has moved on to removing model, then I think the best is to just update the library and remove model (without backward-compatibility). If that's a Z3-specific extension, then probably we should support both the standard and a Z3-specific parser. If that's a Z3-specific extension, it's also possible that they have a flag to behave in an SMT-LIB-complient way, if that's the case the best is probably to run them in this mode.

That's all theoretical because I haven't checked the latest developments in Z3/SMT-LIB. I'll try to take a look when I have some time.

[regb]

Actually it's much simpler than that, https://github.com/regb/scala-smtlib/pull/39/commits should be handling both cases fine.

[acieroid]

Thank you for taking the time to fix it!