Heisenbug with smt-switch boolector backend

[makaimann]

In certain (supposedly rare cases) running BMC with the boolector backend will return an incorrect result. Reproducible on this branch: https://github.com/upscale-project/cosa2/tree/debugging. Small changes, such as adding/removing a print statement that just prints an arbitrary string, will change the result.

The bug might be in https://github.com/makaimann/smt-switch or in boolector.

[ahmed-irfan]

Is it fixed now?

[lonsing]

@ahmed-irfan @makaimann

Your recent changes to the unroller made in https://github.com/upscale-project/cosa2/pull/42 and https://github.com/upscale-project/cosa2/pull/41 fixed the assertion failures related to the reference counting. Moreover, this also fixes all the assertion failures we had on the instances in the 'samples' directory.

I ported these changes to my debugging setup (https://github.com/lonsing/cosa2/tree/cosa2-refcount-debugging). I will do some more tests.

[ahmed-irfan]

Cool

[ahmed-irfan]

can we close this?

[lonsing]

yes, at least based on my tests, I think we can close it.

[makaimann]

Great! Closing it.