search

caterinaurban / Typpete

34 stars 6 forks source link

Crash when using soft constraints #55

Open adsharma opened 3 years ago

adsharma commented 3 years ago 
typpete /tmp/foo.py / --enable_soft_constraints=0

works ok. But the default behavior with --enable_soft_contraints=true results in a core dump inside Z3_optimize_check().

This is on a vanilla ubuntu 20.04 system with python3.8

caterinaurban commented 3 years ago

The problem might be due to the version of Z3 that you are using. We have yet to update Typpete to work with the latest versions. The last Z3 version that we are sure works is version 4.5.1. I am sorry about that!

adsharma commented 3 years ago

Using system z3 instead of the one included in the git repo seems to work ok on a simple test program. But some unittests break.

https://github.com/adsharma/Typpete/commit/ffa65db52c126f8ae3d7c5593192f1adc1ef0567

caterinaurban commented 3 years ago

Which version of Z3 is that? Thank you!

adsharma commented 3 years ago

4.8.12.0 as per https://pypi.org/project/z3-solver/#history

I suspect the pypi packages come from https://github.com/angr/angr-z3

adsharma commented 3 years ago

I figured out how to run the tests. 60 passes and 1 failure. Both before and after.

https://paste.ubuntu.com/p/RxRd2czrZ8/

adsharma commented 3 years ago

The one failing test passes after:

https://github.com/adsharma/Typpete/commit/15bef9810ecf244b8d3fab8ad3f10436209ccb46

I'm not sure exactly why.