Segfaults in Bitwuzla #570
Description
Hello,
there are some intermittent segfaults when using Bitwuzla in CPAchecker. Here is an example stack trace:
Native frames: (J=compiled Java code, j=interpreted, Vv=VM code, C=native code)
C [libbitwuzlaj.so+0x41af38] bzla::type::TypeManager::garbage_collect(bzla::type::TypeData*)+0x28
Java frames: (J=compiled Java code, j=interpreted, Vv=VM code)
J 5363 org.sosy_lab.java_smt.solvers.bitwuzla.api.BitwuzlaNativeJNI.delete_Sort(J)V (0 bytes) @ 0x00007ccadc65ebe9 [0x00007ccadc65eba0+0x0000000000000049]
J 7441 c2 org.sosy_lab.java_smt.solvers.bitwuzla.api.Sort.finalize()V (5 bytes) @ 0x00007ccadc5233f4 [0x00007ccadc523320+0x00000000000000d4]
J 8473% c2 java.lang.ref.Finalizer$FinalizerThread.run()V java.base@23-ea (39 bytes) @ 0x00007ccadc584e30 [0x00007ccadc584b20+0x0000000000000310]
v ~StubRoutines::call_stub 0x00007ccadbf38cc6
The problem is non-deterministic and hard to reproduce. It may be linked to floating-point Sort objects that get garbage collected to early. We should try disabling the Sort finalizer to see if it makes any difference