Простое упражнение Z3, возвращающее неизвестное значение

Я начинаю использовать решатели SMT, и я практиковался с этой простой проблемой:

Exercise 5. Using Z3 at the restaurant:
(a) Encode the following menu choices into Z3 and determine what a customer could buy using exactly
$15.05
• Mixed fruit $2.15
• French Fries $2.75
• Side Salad $3.35
• Hot Wings $3.55
• Mozzarella Sticks $4:20
• Sampler Plate $5:80
(b) Is it possible to order everything on the menu?
(c) Does this problem have only one solution? If it does
 not, what are the other solutions? 

Мое решение для а) таково:

from z3 import *

fruit = Real('fruit')
fries = Real('fries')
salad = Real('salad')
wings = Real('wings')
mozzarella = Real('mozzarella')
sampler = Real('sampler')

Total= Real('total')

multiplier1= Int("mul1")
multiplier2= Int("mul2")
multiplier3= Int("mul3")
multiplier4= Int("mul4")
multiplier5= Int("mul5")
multiplier6= Int("mul6")

x = Real('x')
y = Real('y')
s = Solver()
s.add(multiplier1*fruit + multiplier2*fries + multiplier3*salad + multiplier4*wings + multiplier5*mozzarella + multiplier6*sampler == 15.05)


print(s.check())
print(s.model())

Но он возвращает unknown. Почему??

Решение для б):

from z3 import *

fruit = Real('fruit')
fries = Real('fries')
salad = Real('salad')
wings = Real('wings')
mozzarella = Real('mozzarella')
sampler = Real('sampler')

Total= Real('total')

multiplier1= Int("mul1")
multiplier2= Int("mul2")
multiplier3= Int("mul3")
multiplier4= Int("mul4")
multiplier5= Int("mul5")
multiplier6= Int("mul6")


s = Solver()
s.add(multiplier1*fruit + multiplier2*fries + multiplier3*salad + multiplier4*wings + multiplier5*mozzarella + multiplier6*sampler == 15.05)
s.add(multiplier1>0)
s.add(multiplier2>0)
s.add(multiplier3>0)
s.add(multiplier4>0)
s.add(multiplier5>0)
s.add(multiplier6>0)


print(s.check())
print(s.model())

Тот же результат! :(

Решение для c): сначала мне нужно получить решения :'(

Это очень простая проблема. Что я делаю не так?

ПРИМЕЧАНИЕ. Упражнение получено с: http://www.loria.fr/~mery/malg/Z3.pdf Спасибо.

РЕШЕНИЕ:

from z3 import *

fruit = Real('fruit')
fries = Real('fries')
salad = Real('salad')
wings = Real('wings')
mozzarella = Real('mozzarella')
sampler = Real('sampler')

multiplier1= Int("mul1")
multiplier2= Int("mul2")
multiplier3= Int("mul3")
multiplier4= Int("mul4")
multiplier5= Int("mul5")
multiplier6= Int("mul6")

s = Solver()
s.add(multiplier1*fruit + multiplier2*fries + multiplier3*salad + multiplier4*wings + multiplier5*mozzarella + multiplier6*sampler == 15.05)
s.add(fruit==2.15)
s.add(fries==2.75)
s.add(salad==3.35)
s.add(wings==3.55)
s.add(mozzarella==4.20)
s.add(sampler==5.80)
s.add(multiplier1>=0)
s.add(multiplier2>=0)
s.add(multiplier3>=0)
s.add(multiplier4>=0)
s.add(multiplier5>=0)
s.add(multiplier6>=0)

while s.check() == sat:
  print s.model()
  s.add(Or(multiplier1 != s.model()[multiplier1], multiplier2 != s.model()[multiplier2] ,multiplier3 != s.model()[multiplier3] , multiplier4 != s.model()[multiplier4] ,multiplier5 != s.model()[multiplier5], multiplier6 != s.model()[multiplier6])) # prevent next model from using the same previous one