CODEWITHSUNDEEP
z3z3py
Fuxiang Chen
Fuxiang Chen

Reputation: 83

z3.z3types.Z3Exception: model is not available

I'm using the latest z3py build release (x64) in Win10 x64, python 2.7 x64.

When I try to call model on this constraint:

(i2 % 59) == (i2 * i10) , (i10 % 43) == ((i2 + i12) % 3) , 4 != (i14 % 28) , 
5 != (i14 % 28) , 6 != (i14 % 28) , 7 != (i14 % 28) , 8 != (i14 % 28) , (i2 
- i12) >= (i12 + i10) , ((i2 - i1) - (i2 * i1)) >= (i1 - 50) , (i12 - i2) < 
(i2 * i12)

It throws the following exception:

z3.z3types.Z3Exception: model is not available.

All the variables (e.g. i2, i10, etc are Integer)

I noted that check produce empty for this constraint.

Does that mean that this constraint is unsat?

Upvotes: 3

Views: 4596

Answers (1)

Fuxiang Chen
Fuxiang Chen

Reputation: 83

check needs to be called first, and only if it returns SAT there will be a model.

From @Christoph's comment.

Thanks.

Upvotes: 4

Related Questions