search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.22k stars 1.47k forks source link

Possible regression between 4.12.1 and 4.13.0 #7255

Closed blishko closed 3 weeks ago

blishko commented 3 months ago

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 commented 3 months ago

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 commented 2 months ago

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

hgvk94 commented 2 months ago

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

hgvk94 commented 2 months ago

[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 commented 2 months ago

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 commented 3 weeks ago

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!