[SMT-LIB] SMT doubt: Fibonacci example

[Yeting Ge]

Hi Daniela,

As for the first query, do you mean the negation of it?
It is assumed in SMT to check satisfiability, not validity.
To me the assumptions and the first query are consistent.

Thank you,
Yeting

On Mon, 1 Sep 2008, Daniela da Cruz wrote:

> Hello all.
> I'm trying to translate Fibonacci example from Java+JML to SMT (this
> translation is done according with some theoretical formulas).
> But unfortunately for each formula that I have on benchmark the result is
> "unknown".
> I send the SMT code in attach.
> Can anyone help me?
>
> Best regards,
>
> daniela
>