Sylvan : Crash in Lib-BDD reconstruction

[SSoelvsten]

Sylvan seems to crash due to a LACE Stack overflow during the reconstruction of the input for the RelProd benchmark. This would presumably also happen in the Apply benchmark.

[jacopol]

Could increase the stacksize through ulimit -s <size> (in KiB?)

[SSoelvsten]

The only operation that is used during reconstruction of the input (serialized BDDs) is the ITE . Simultaneously, the BDD is built bottom-up, meaning the ITE should take O(1) . Hence, the issue is something much more subtle and weird.

[SSoelvsten]

The issue lies in the fact, that Sylvan's garbage collection has the following undocumented assumption:

The number of BDD roots (i.e. references from the user's program) is smaller than the size of the Lace queue.

Hence, Sylvan breaks when the vector<sylvan:Bdd> out in common/libbdd_parser.h::reconstruct<Adapter>(...), which contains all BDD nodes for reconstruction, is larger than the Lace stack.

[SSoelvsten]

Merging that PR does not fully resolve the issue - just push the boundary of what Sylvan can deserialize. Closing this was not the intention.