z3.z3types.Z3Exception: Modell ist nicht verfügbar

Question

Ich benutze die neueste z3py Build-Version (x64) in Win10 x64, Python 2.7 x64.

Wenn ich versuche, model auf diese Einschränkung zu nennen:

(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) 

Es wirft die Ausnahme z3.z3types.Z3Exception: model is not available.

Alle Variablen (z.B. i2, i10, etc sind Integer)

I angemerkt, dass für diese check constraint leer erzeugen.

Bedeutet das, dass diese Bedingung nicht erfüllt ist?

Danke für Hilfe.

Answer 1

check muss zuerst aufgerufen werden, und nur wenn es SAT zurückgibt, wird es ein Modell geben.

Aus @ Christophs Kommentar.

Danke.