Yices crashes during interpolation #615
Description
Hello,
We've seen some occasional crashes during interpolation. The problem appears to be deterministic, however, I've been having a hard time finding a minimal example that will trigger the crash. What I can provide for now is a stacktrace:
Stack: [0x00007106186cc000,0x00007106187cc000], sp=0x00007106187c9400, free space=1013k
Native frames: (J=compiled Java code, j=interpreted, Vv=VM code, C=native code)
C [libyices2java.so+0x17b787] mcsat_decide_assumption+0x403
C [libyices2java.so+0x17c996] mcsat_solve+0x487
C [libyices2java.so+0x59efb] check_context_with_model+0x5a
C [libyices2java.so+0x37cad] _o_yices_check_context_with_model+0x1c9
C [libyices2java.so+0x37d4e] yices_check_context_with_model+0x54
C [libyices2java.so+0x3827a] yices_check_context_with_interpolation+0x160
C [libyices2java.so+0x1e982] Java_com_sri_yices_Yices_checkContextWithInterpolation+0x102
j com.sri.yices.Yices.checkContextWithInterpolation(JJJ[J[I)I+0
j com.sri.yices.InterpolationContext.check(Lcom/sri/yices/Parameters;Z)Lcom/sri/yices/Status;+53
When assertions are enabled, this message is printed instead:
mcsat/value.c:478: mcsat_value_construct_from_value: Assertion `false' failed.
I've been using issue-613-mcsat-curried-function-model for my tests as I initially thought the problem may be related. However, it still seems to happen, even with the new branch
Do you have an idea what could be causing the issue?