Typpete Crash when using soft constraints

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

Jul 03 '21 23:07 adsharma

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!

Jul 12 '21 10:07 caterinaurban

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

Jul 20 '21 20:07 adsharma

Which version of Z3 is that? Thank you!

Jul 21 '21 11:07 caterinaurban

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

Jul 21 '21 16:07 adsharma

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

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

Jul 21 '21 18:07 adsharma

The one failing test passes after:

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

I'm not sure exactly why.

Jul 22 '21 17:07 adsharma