Elias Kuiter

I have the same issue. Any updates?

another small issue: right now, `setup.py` does not restrain the z3 solver version, so the newest version (4.12.1) is used. but in this version (4.11.2 behaves differently), the call to...

AFAICT, it should work. i can't execute your code (pickle.load fails with `TypeError: a bytes-like object is required, not 'str'`) on a Linux 2.6.32 kclause file like this ``` config...

` UnicodeDecodeError: 'ascii' codec can't decode byte 0x80 in position 0: ordinal not in range(128) ` i think Github broke it somehow by assuming it's a txt :shrug: maybe as...

I still can't get it to work, not sure what is going on: ```UnicodeDecodeError: 'utf-8' codec can't decode byte 0x80 in position 0: invalid start byte``` Here's my Docker script:...

I have looked at your file and can reproduce the issue. But I am still not able to find the problem. When I remove constraints from the file, at some...

I tried another approach and now have a minimum failing example, although it still has over 2000 constraints: [docker-test-branch.zip](https://github.com/paulgazz/kmax/files/10922754/docker-test-branch.zip) I exported it into SMTLib and removed all non-boolean variability: [min-bool.smt.txt](https://github.com/paulgazz/kmax/files/10922775/min-bool.smt.txt)...

Until we have a better solution, my workaround is to use z3 4.11.2, where the above works fine.

same here (Chrome / Mac with gridfs / dropbox)

I tested the Cypress FM24CL16B with an ESP32. Works like a charm.