[SMT-LIB] SMT doubt: Fibonacci example

Yeting Ge yeting at courant.nyu.edu
Mon Sep 1 16:13:39 EDT 2008


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
>


More information about the SMT-LIB mailing list