Python API lingeling assertion hit watcher stack overflow

[edcote]

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

[edcote]

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.

[edcote]

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.

[edcote]

https://github.com/Boolector/boolector/pull/170

[arminbiere]

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).