Запрос Z3 с экзистенциальным квантификатором возвращает неверный результат

Question

Я построил следующее

s=Solver()
s.add(ForAll([n],Implies(n>=0,x(n + 1) == If((x(n)==0),0,1))))
s.add(x(0) == 0)
s.add(Not(Exists([n],Implies(n>=1,(x(n)!=0)))))

Приведенный выше запрос возвращает unsat, что, по-видимому, неверно?

Аналогично

s=Solver()
s.add(ForAll([n],Implies(n>=0,x(n + 1) == If((x(n)==0),1,1))))
s.add(x(0) == 0)
s.add(Not(Exists([n],Implies(n>=1,(x(n)!=0)))))

Приведенный выше запрос возвращает unsat, что, по-видимому, неверно?

Пожалуйста, помогите мне понять, что не так в вышеуказанных запросах?

Answer 1

Только ваш экзистенциал уже неудовлетворителен, что может быть более очевидным, если вы замените импликацию if-then-else:

not exists n :: 1 <= n ? x(n) != 0 : true

Таким образом, для любого n < 1 вы предполагаете, что

not exists n :: true

Это явно не так.