search

kino-mc / rsmt2

A generic library to interact with SMT-LIB 2 compliant solvers running in a separate system process, such as Z3 and CVC4.
Apache License 2.0
65 stars 14 forks source link

fix parser for Z3 4.8.10 #25

Closed ryosu-sato closed 3 years ago

ryosu-sato commented 3 years ago

Z3 does not output the string "model" when (get-model) from the version 4.8.10. I changed parse.rs to accept Z3's outputs without "model".

AdrienChampion commented 3 years ago

Nice, thanks!