Model not available exception s.check() is returning 'sat'

[Ipsita Koley]

I am using z3py.

s.check() is returning 'sat' however it is giving the following exception

Traceback (most recent call last):

  File "understeerSlow.py", line 3788, in <module>

    m = s.model()

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

    raise Z3Exception("model is not available")

z3types.Z3Exception: model is not available

[Michael Tautschnig]

Hello,

I’m not sure how your question relates to CPROVER/CBMC?

Best,

Michael

--

---
You received this message because you are subscribed to the Google Groups "CProver Support" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cprover-suppo...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/cprover-support/9fbe8159-b3d9-4b92-9178-9342899d10d4%40googlegroups.com.

[Ipsita Koley]

Mistakenly I posted the topic in this group.

Anyway, if anybody knows the solution it would be an immense help