Bruno Dutertre

Thanks for the comments @aman-goel! We're a bit busy with other things right now so it may take a while before we digest it all. Hope you find sally useful.

That sounds like a reasonable feature but that may take a while to implement. We'd have to go through all our data structures and implement a clone method for them.

Hi Aman, The solver should be able to handle arbitrary arrays so that should work. Just remember that SMT-LIB 2 does not allow symbols (including sort names) to start with...

Thanks for reporting this. We'll rename 'NO_ERROR' to something else in the next release.

Hi @weaversa, ``bv2nat`` is not part of the official SMTLIB QF_BV logic. It cannot be part of this logic since it requires natural numbers in addition to bit-vectors. The bv2nat...

It's a known issue with linear integer arithmetic. Yices sometimes goes into an infinite branch because its branch algorithm is too crude.

No need to apologize. Thanks for reporting the problem.

This means that Yices doesn't have a value for s1 in the model. I'll check why this happens in this case.

@LeventErkok: A simple work-around is to change the logic to QF_ABV instead of QF_UFBV. In your example, variable ``s1`` is eliminated. When you ask for its value, Yices tries to...

Do you have `/usr/local/lib/libcudd.a`?