Python API lingeling assertion hit watcher stack overflow
edcote opened this issue · 4 comments
EDIT: Different assertion hit when NDEBUG removed. Still suspect its something at the interface of Pyboolector and Boolector.
Could anyone help shed some light on the following assertion failure in lingeling?
Quite likely this is a build environment problem on my end. Unfortunately, I am not all that familiar with Python extensions, booletor, or lingeling.
My assumption is some structure is not being passed properly between Python and boolector.
Anyone have any clue on where/how I should start looking?
def test_should_work(self):
btor = pyboolector.Boolector()
x = btor.Var(btor.BitVecSort(2), "x") // <--- this does NOT die for BitVecSort(1)
btor.Assert(0 < x)
result = btor.Sat()*** internal error in 'third_party/lingeling/lglib.c': watcher stack overflow
static ptrdiff_t lglenlwchs (LGL * lgl, HTS * hts) {
int oldhcount, ldoldhcount, ldnewhcount, newhcount;
long oldwcount, newwcount, oldwsize, newwsize;
int * oldwstart, * newwstart, * start;
unsigned oldoffset, newoffset, i, j;
ptrdiff_t res;
res = 0;
oldhcount = hts->count;
oldoffset = hts->offset;
newhcount = 1, ldnewhcount = 0;
ldoldhcount = lglfloorld (oldhcount);
assert (ldoldhcount < 31);
ldnewhcount = ldoldhcount + 1;
if (ldnewhcount > 30) lgldie (lgl, "watcher stack overflow"); // <-- HIT this assertion
*** Check failure stack trace: ***
@ 0x55a463a1e552 lglpushwch
@ 0x55a463a1d7c0 lglwchtrn
@ 0x55a463a1c127 lgladdcls
@ 0x55a4639f8d45 lgleadd
@ 0x55a4639f803f lgladd
@ 0x55a4639e3d6f add
@ 0x55a4639743ee btor_sat_add
@ 0x55a46390395b btor_aig_to_sat_tseitin
@ 0x55a463907e5d btor_aigvec_to_sat_tseitin
@ 0x55a46392b0f1 btor_synthesize_exp
@ 0x55a4639271a6 exp_to_aig
@ 0x55a463927053 btor_process_unsynthesized_constraints
@ 0x55a463979760 sat_fun_solver
@ 0x55a46392bff5 btor_check_sat
@ 0x55a4638e1a86 boolector_sat
@ 0x7fe67f4edf61 __pyx_pw_11pyboolector_11pyboolector_9Boolector_29Sat()
@ 0x55a463def703 _PyCFunction_FastCallDict
@ 0x55a463e7b8a5 call_function
@ 0x55a463e78879 _PyEval_EvalFrameDefault
@ 0x55a463e7d091 _PyFunction_FastCall
@ 0x55a463e7b87f call_function
@ 0x55a463e78879 _PyEval_EvalFrameDefault
@ 0x55a463e7c301 _PyEval_EvalCodeWithName
@ 0x55a463e7cf1a _PyFunction_FastCallDict
@ 0x55a463d9f1dd _PyObject_FastCallDict
@ 0x55a463d9f4a6 _PyObject_Call_Prepend
@ 0x55a463d9ef6b PyObject_Call
@ 0x55a463e78aa7 _PyEval_EvalFrameDefault
@ 0x55a463e7c301 _PyEval_EvalCodeWithName
@ 0x55a463e7cf1a _PyFunction_FastCallDict
@ 0x55a463d9f1dd _PyObject_FastCallDict
@ 0x55a463d9f4a6 _PyObject_Call_Prepend
@ 0x55a463d9ef6b PyObject_Call
@ 0x55a463e0a598 slot_tp_call
@ 0x55a463d9f2c5 _PyObject_FastCallDict
@ 0x55a463e7b878 call_function
@ 0x55a463e78879 _PyEval_EvalFrameDefault
@ 0x55a463e7c301 _PyEval_EvalCodeWithName
@ 0x55a463e7cf1a _PyFunction_FastCallDict
@ 0x55a463d9f1dd _PyObject_FastCallDict
@ 0x55a463d9f4a6 _PyObject_Call_Prepend
@ 0x55a463d9ef6b PyObject_Call
@ 0x55a463e78aa7 _PyEval_EvalFrameDefault
@ 0x55a463e7c301 _PyEval_EvalCodeWithName
@ 0x55a463e7cf1a _PyFunction_FastCallDict
@ 0x55a463d9f1dd _PyObject_FastCallDict
@ 0x55a463d9f4a6 _PyObject_Call_Prepend
@ 0x55a463d9ef6b PyObject_Call
@ 0x55a463e0a598 slot_tp_call
@ 0x55a463d9f2c5 _PyObject_FastCallDict
@ 0x55a463e7b878 call_function
@ 0x55a463e78879 _PyEval_EvalFrameDefault
@ 0x55a463e7c301 _PyEval_EvalCodeWithName
@ 0x55a463e7cf1a _PyFunction_FastCallDict
@ 0x55a463d9f1dd _PyObject_FastCallDict
@ 0x55a463d9f4a6 _PyObject_Call_Prepend
@ 0x55a463d9ef6b PyObject_Call
@ 0x55a463e78aa7 _PyEval_EvalFrameDefault
@ 0x55a463e7c301 _PyEval_EvalCodeWithName
Likely cause is my lingeling version is out of date.
static const char lglfloorldtab[256] =
{
// 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
-1, 0, 1, 1, 2, 2, 2, 2, 3, 3, 3, 3, 3, 3, 3, 3,
LT(4), LT(5), LT(5), LT(6), LT(6), LT(6), LT(6),
LT(7), LT(7), LT(7), LT(7), LT(7), LT(7), LT(7), LT(7)
};
I picked up the version in contrib/setup_lingeling.sh. That may need to be updated. Will look tomorrow.
The issue is
ldoldhcount = lglfloorld (oldhcount); // input 0 returns -1 cast to unsigned char is 255
assert (ldoldhcount < 31); // fails this if assertions as enabled
ldnewhcount = ldoldhcount + 1;
if (ldnewhcount > 30) lgldie (lgl, "watcher stack overflow"); // this assertion also fails.
Just as reference for future such issues. If it had been an issue with Lingeling then having a Lingeling API call trace would have helped. This can be generated by setting the environment variable 'LGLAPITRACE' to point to a file where the traces is saved. One might need to avoid generating multiple Lingeling instances though (by for instance disable certain preprocessing options).