Bruno Dutertre

I don't think you screwed up anything. The problem is that you have two versions of libcudd. That doesn't happen to me. I only get 'libcudd.a' (but I always build...

Interesting. I thought ``--disable-shared`` was the default for cudd. When I run ``./configure`` in cudd (without any flags), it prints this: ``` -------------------------------------------------- Configuration summary for cudd 3.0.0 Build system...

The tricky part is to get a pic version of libgmp.a. If you already have one, I wouldn't upgrade to a new version of GMP. Otherwise, the latest GMP should...

Thanks. but can you also include the ``mkConstraint`` function?

@baierd. Did you see our previous question: what's ``mkConstraint``?

I'm more worried about the calls to ``yices_init`` and ``yices_exit``. You shouldn't call them more than once per JVM. Are there other @Test methods running concurrently?

Probably just an omission.

Thanks. We have experimented with tcmalloc in the past. I didn't know the difference was that large.

That should be feasible, but it will take some time.

Don't use recursive functions. Yices will not support them any time soon. Here's why: 1) simple logics that are decidable become undecidable if you allow recursive functions. 2) to do...