z3py issue

[Ipsita Koley]

File "understeerSlow_withCriteria.py", line 5782, in <module>

    m = s.model()

  File "/usr/lib/python2.7/dist-packages/z3/z3.py", line 6547, in model

    raise Z3Exception("model is not available")

This error is coming however s.check() returns "sat"

[Andrea Micheli]

Dear Ipsita,

this seems a problem with z3py, not pysmt (http://pysmt.org).

Anyhow, it's hard to suggest for solutions without seeing your code, but here are a few tips:

- You NEED to call s.check() BEFORE you can call s.model()

- check that model-generation is enabled  (e.g. if you are parsing an SMT2 file check is the option produce-models is set to true)

HTH

Andrea

--
You received this message because you are subscribed to the Google Groups "pySMT" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pysmt+un...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/pysmt/f9a37ce7-8e76-4d10-811a-a698ff74c4f8%40googlegroups.com.