Baier D.

Simply use the formulas in the assert statements in an array with the `yices_check_context_with_assumptions()` method. I've updated the code above. Is there any helpful difference in how Yices2 asserts formulas...

I am an idiot, sorry. ``` int mkConstraint(int newIdx, int increment, int selector) { String COUNTER_PREFIX = "c@"; return yices_and2( selector, yices_eq( yices_named_variable(yices_int_type(), COUNTER_PREFIX + newIdx), yices_add( yices_named_variable(yices_int_type(), COUNTER_PREFIX +...

I can confirm that there is no "SAT" problem in your program on my machine(I've tested your program with my lib). The problem could be the build/recompilation used after creating...

A little context: I work at the [JavaSMT](https://github.com/sosy-lab/java-smt/tree/yices2) project. We are providing a unified API for multiple SMT-Solvers. We use a selfmade JNI wrapper that simply handels input/output into Yices2....

The context created in `CreateEnvironment` is not used by the concurrency test below (Its simply ignored and deleted later. We use that for the other tests but they are not...

`yices_init` and `yices_exit` are called only once at the beginning of a test and at the very end. The concurrency is handled inside the @Test. So from the point of...

Also, Yices2 supports arrays, while we do not. We should update Yices2 and incorporate arrays (and other new features).

By the way, with your additions in #325 , we could easily provide a default implementation for this feature.

We should split the 2 matters and include the FP fixes in the add_bitwuzla branch and PR. And we need to check/discuss if we want auto-generated wrappers. They are quite...

This looks like a bug in CVC5. Because what fails is our preconditions `Preconditions.checkArgument(sort.equals(exp.getSort()), ...)` second argument `exp.getSort()`, as it equals null. So CVC5 can not find the Sort of...