Lingeling watcher stack overflow with basic rand constraint?

[edcote]

Wondering whether anyone has come across this and/or can provide some tips on how to debug.

My presumption is the failure is due to my build environment, to not pyvsc itself.

@vsc.randobj
class Config:
  def __init__(self):
    self.widths = vsc.rand_list_t(vsc.bit_t(2), 5)  # bit_t() does NOT fail

  @vsc.constraint
  def c(self):
    with vsc.foreach(self.widths) as it: it > 0

static ptrdiff_t lglenlwchs (LGL * lgl, HTS * hts) {
[..]
  newhcount = 1, ldnewhcount = 0;
  ldoldhcount = lglfloorld (oldhcount);
  assert (ldoldhcount < 31);
  ldnewhcount = ldoldhcount + 1;
  if (ldnewhcount > 30) lgldie (lgl, "watcher stack overflow"); // <---- HIT THIS
  newhcount = (1<<ldnewhcount);

Here is the stack trace .....

assert.h assertion failed at [..] lglib.c:3740 in

ptrdiff_t lglenlwchs(LGL *, HTS *): ldoldhcount < 31

*** Check failure stack trace: ***
    @     0x5565ddbd1ec4  __assert_fail

    @     0x5565dd5da0a2  lglpushwch
    @     0x5565dd5d9310  lglwchtrn
    @     0x5565dd5d7c77  lgladdcls
    @     0x5565dd5b4968  lgleadd
    @     0x5565dd5b3c2f  lgladd
    @     0x5565dd59f9cf  add
    @     0x5565dd53004e  btor_sat_add
    @     0x5565dd4bf5bb  btor_aig_to_sat_tseitin
    @     0x5565dd4c3abd  btor_aigvec_to_sat_tseitin
    @     0x5565dd4e6d51  btor_synthesize_exp
    @     0x5565dd4e2e06  exp_to_aig
    @     0x5565dd4e74a7  btor_add_again_assumptions
    @     0x5565dd535406  sat_fun_solver
    @     0x5565dd4e7c55  btor_check_sat
    @     0x5565dd49d6e6  boolector_sat

    @     0x7fac4f703f61  __pyx_pw_11pyboolector_11pyboolector_9Boolector_29Sat()

    @     0x5565ddad7703  _PyCFunction_FastCallDict
    @     0x5565ddb638a5  call_function
    @     0x5565ddb60879  _PyEval_EvalFrameDefault
    @     0x5565ddb64301  _PyEval_EvalCodeWithName
    @     0x5565ddb64c68  fast_function
    @     0x5565ddb6387f  call_function
   [..]
    @     0x5565ddb60879  _PyEval_EvalFrameDefault
    @     0x5565ddb64301  _PyEval_EvalCodeWithName
    @     0x5565ddb5ab64  PyEval_EvalCodeEx
    @     0x5565ddabbc26  function_call
    @     0x5565dda86f6b  PyObject_Call
    @     0x5565dda87d6b  callmethod
    @     0x5565dda87c4c  PyObject_CallMethod

[edcote]

Initial Model:
  <anonymous> {
    unsigned [32] size
    bayer_input_widths {
        rand unsigned [2] <unknown>[0]
        rand unsigned [2] <unknown>[1]
    }
    constraint c_frame_size {
        foreach (bayer_input_widths[i]) {
            (bayer_input_widths[index] > 0);
        }
    }
}

Final Model:
  <anonymous> {
    unsigned [32] size
    bayer_input_widths {
        rand unsigned [2] <unknown>[0]
        rand unsigned [2] <unknown>[1]
    }
    constraint c_frame_size {
        (bayer_input_widths.<unknown>[0] > 0);
        (bayer_input_widths.<unknown>[1] > 0);
    }
}

RandSet
  Field: bayer_input_widths.<unknown>[0] [[1, 3]]
  Constraint: (bayer_input_widths.<unknown>[0] > 0);

RandSet
  Field: bayer_input_widths.<unknown>[1] [[1, 3]]
  Constraint: (bayer_input_widths.<unknown>[1] > 0);

Unconstrained: size
Pre-Randomize: RandSet
  Field: bayer_input_widths.<unknown>[0] [[1, 3]]
  Constraint: (bayer_input_widths.<unknown>[0] > 0);

Pre-Randomize: RandSet
  Field: bayer_input_widths.<unknown>[1] [[1, 3]]
  Constraint: (bayer_input_widths.<unknown>[1] > 0);

[edcote]

Not pyvsc related. Reproducible directly on pyboolector API.