pysmt: Non-deterministic segfault of tests with Z3 in Travis
I noted that the builds having the z3 solver can non-deterministically yield a segfault on Travis.
I tried to reproduce the problem locally even using the docker Travis image with no luck.
We could try two different strategies here:
- Update Z3 to a newer nightly build and see if the problem goes away
- Try to update the libstdc++ of the travis image (it is more a feeling than a suspect, but in my local experiment with the
quay.io/travisci/travis-pythondocker image I had to update this to make Z3 work at all)
About this issue
- Original URL
- State: open
- Created 7 years ago
- Comments: 22 (16 by maintainers)
Commits related to this issue
- Disabled another tests that was using tactics and was causing issues see #465 — committed to pysmt/pysmt by mikand 5 years ago
- Re-enabled tests in the hope of fixing #465 — committed to pysmt/pysmt by mikand 5 years ago
- Workaround to fix Z3 segfault discovered in discussion on #465 — committed to pysmt/pysmt by mikand 2 years ago
- Disabled another tests that was using tactics and was causing issues see #465 — committed to nbailluet/pysmt by mikand 5 years ago
- Re-enabled tests in the hope of fixing #465 — committed to nbailluet/pysmt by mikand 5 years ago
- Workaround to fix Z3 segfault discovered in discussion on #465 — committed to nbailluet/pysmt by mikand 2 years ago
@marcogario Just to clarify: the issue is now fixed on the pysmt side with the workaround in #713. @Hook25 (many thanks!) posted the issue upstream, if/when Z3 fixes the issue we can get rid of the workaround.
I think I finally isolated the issue! On #564 I disabled the test
test_tactics_z3intest_solving.pyand since then I got no more segfault errors. This smells of victory because the test actually accesses the internal Z3 nodes and applies a custom tactic, so it may very well mess up the ref/deref system.I still have no clear explanation/fix of the problem, but I’ll have a look asap.