[SMT-LIB] SMT doubt: Fibonacci example

[Daniela da Cruz]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Fibonacci.smt
Type: application/octet-stream
Size: 776 bytes
Desc: not available
Url : /pipermail/smt-lib/attachments/20080901/8053ae04/Fibonacci.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Fibonacci3.java
Type: text/x-java
Size: 589 bytes
Desc: not available
Url : /pipermail/smt-lib/attachments/20080901/8053ae04/Fibonacci3.bin