Hello everyone,

We would like to use MC-SAT in Yices with the thread-safe API option. The documentation says that --enable-mcsat and --enable-thread-safety can't be combined, but the check in the configure script has been removed some time ago, and it's possible to build the binary with both options

While testing, the binary seems to work mostly just fine. However, there were some issues when generating unsat core with MCSAT, where Yices seems to deadlock when --enable-thread-safety was used while compiling the binary. We also saw some segfaults outside of unsat core, but these may be caused by a different issue

Are these issues just because unsat core is still new for MC-SAT? Or should --enable-mcsat and --enable-thread-safety simply not be combined?

Thank you advance,
Daniel