Possible regression between 4.12.1 and 4.13.0

[blishko]

Hi @NikolajBjorner , @agurfinkel!

In SolCMC, we have observed some regressions on our test suite when attempting to upgrade Z3 from 4.12.1 to 4.13.0. I have prepared a simplified example here. When running z3 with the option fp.xform.inline_eager=false, version 4.13.0 hangs, while version 4.12.1 solves it immediately. Note that both fp.xform.inline_eager=false and (set-option :produce-proofs true) in the file are required for 4.13.0 to hang.

Let me know, if I should try to minimize the example even further. I could spend more time on this, if the cause is not anything obvious.

[agurfinkel]

Adding @hgvk94 . Hari had some local changes that have not yet been migrated to master. We need to check whether they address the issue.

[blishko]

Would it help if I try to minimize the example further?

[hgvk94]

Thanks. The example is simple enough. Looks like Spacer is getting stuck in the proof generation phase. Debugging this ...

[hgvk94]

[updates] Spacer is getting stuck in an SMT query made to the solver during proof generation. The query is here. This is commit that introduced this problem: https://github.com/Z3Prover/z3/commit/d0d434e4f1fc847abc38940f4a9e6d97bf1ec44a Debugging it now ...

[hgvk94]

The problem is when creating a model for an array expression. The final_check method attempts to merge all enodes that are not equal here. However, with the new is_unique_value implementation in d0d434e, the mk_eq_atom method returns false. Now the array solver thinks it merged two enodes together by adding a new equality atom, but in reality, it's just adding false. This causes an infinite loop in the final_check method

[blishko]

I have tried rerunning the benchmarks with master and they now work fine. I am closing this issue and I am looking forward to a new release!