Name of constants affects satisfiability result when using Python API

[aengelke]

When using hexadecimal random uuids (using uuid.uuid4().hex in Python) as part of the names of the constants, I noticed that an otherwise identical constraint system leads to different results depending on the names, i.e. sometimes gives sat and sometimes unsat.

I extracted an example which shows these differences, and also generated the Z3 logs for both cases (sat and unsat) using z3.open_log. Unfortunately, I wasn't able to reduce the size of this example.

Let me know if I can provide any further information.

System: Debian 9 (Stretch), x86-64
Z3: master (dca30ab), release build
Python 2.7.13

bugdata.zip

[NikolajBjorner]

I get an assertion violation in one of the traces at the same place as #1233. Are these bugs related?

[aengelke]

It might perfectly be the case that both issues have the same cause. If so, feel free to close one of the two issues. (When compiling in debug mode, I also get an assertion failure in src/smt/smt_conflict_resolution.cpp:580.)

[NikolajBjorner]

I presume this is a duplicate of #1233, which was now fixed.