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

8 views
Skip to first unread message

Ipsita Koley

unread,
Aug 4, 2019, 2:58:22 AM8/4/19
to CProver Support
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

unread,
Aug 4, 2019, 6:09:07 AM8/4/19
to cprover...@googlegroups.com
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

unread,
Aug 4, 2019, 6:12:07 AM8/4/19
to CProver Support
Mistakenly I posted the topic in this group.
Anyway, if anybody knows the solution it would be an immense help
Reply all
Reply to author
Forward
0 new messages