solverCheckAndGetModel segfaults on timeout

[deian]

solverCheckAndGetModel segfaults on timeout. Might we worth only calling getModel when sat:

                  Unsat -> return Nothing
                  _     -> Just <$> solverGetModel ctx solver

[IagoAbal]

OK, interesting. Have you tried reporting this to Z3's people? Citing the documentation:

The error handler is invoked if a model is not available because the commands above were not invoked for the given solver, or if the result was Z3_L_FALSE.

Requesting a model when Z3_solver_check returns Z3_L_UNDEF is not supposed to give you a segfault, as far as I can tell.

Nowadays I'm a bit disconnected with the SMT-world but as far as I remember one could get a model from an undefined result. Perhaps requires to set an option or something.

[deian]

We have a workaround in our fork for now, but we're planning on writing new, type-safe bindings for smt; will let you know once we figure it out and maybe our changes can be useful to you!

[IagoAbal]

Sure, please submit a pull request if you have a proposal to fix it. I would very much appreciate it. In this case the correct fix IMO is to make solverGetModel in Z3.Base to check for errors. I guess there are Undef cases were you have no model available.

Regarding the type-safe bindings. I would be very happy to see a type-safe alternative. It depends how much type-safe you want to be. We tried that in earlier versions, it was called Z3.Lang, and ended up removing it. It is easy when you restrict yourself to a subset of SMT theories. It gets tricky and kind of hacky to handle functions and other stuff. Most people using these bindings are building tools, and for that use case too much type-safety can actually be cumbersome to work with. I believe that SBV's author ended up adding an unsafe Dynamic module for that reason.

Then I had plans to make the bindings "safer" even if not type/statically-safe. But I no longer have enough spare time for that!

[deian]

Sounds goo, thanks!