Empty model with Z3 >=4.8

[valderman]

Haskell-Z3 408.0 returns an empty model, even when deciding that a query is satisfiable, when used with Z3 >= 4.8. The problem does not occur with Z3 4.4.

Steps to reproduce

Compile and run the following program:

module Main where
import Control.Monad.IO.Class
import Z3.Monad

main :: IO ()
main = evalZ3 $ do
  a <- mkFreshBoolVar "a"
  b <- mkFreshBoolVar "b"
  assert =<< mkAnd [a, b]
  (result, model) <- withModel modelToString
  liftIO $ do
    print result
    maybe (putStrLn "no model") putStr model

Expected result

The program prints:

Sat
b!1 -> true
a!0 -> true

This is what happens when Z3 4.8 is replaced with 4.4.

Actual result

The program prints:

Sat

Additional details

The problem is not just with modelToString, as calling numConsts on the model returns 0 (and calling getConsts causes a Z3 error: index out of bounds to be thrown).

[IagoAbal]

Thanks for reporting.

Are you saying that Z3 408.0 works as expected with Z3 4.4 but it doesn't print any model with Z3 4.8?

Does it work with the Python API?

[IagoAbal]

If you are able to look into this yourself and submit a patch that would be a lot faster than waiting for me... these days I barely have time to discuss issues and review patches.

[valderman]

Are you saying that Z3 408.0 works as expected with Z3 4.4 but it doesn't print any model with Z3 4.8?

Exactly.

Does it work with the Python API?

I haven't been able to try the Python API, unfortunately. It does work when using the Z3 binary (4.8) however.

If you are able to look into this yourself and submit a patch that would be a lot faster than waiting for me...

I'll look into it if I have the time, but that's a fairly big "if" at the moment I'm afraid.

[IagoAbal]

Unfortunately, the Z3 API changes fairly often and things break. My suggestion would be to "translate" that example to Z3.Base and run it.

I don't have time to look at this either, there is no "if" in my case unfortunately, I just don't have time. The library should be maintained by the ones who need it. But I am happy to donate time in order to help those who want to contribute, like explaining details about the code or reviewing patches.