search

prove-rs / z3.rs

Rust bindings for the Z3 solver.
337 stars 105 forks source link

Update bundled Z3 to z3 4.12.3. #279

Closed waywardmonkeys closed 3 months ago

waywardmonkeys commented 9 months ago

This also changes a test to be less specific about the exact answer since it varies between versions of Z3.

waywardmonkeys commented 9 months ago

cc: @Pat-Lafon

Pat-Lafon commented 9 months ago

The changes look good to me. Are you asking about diffing the windows linking issue?

waywardmonkeys commented 9 months ago

4.12.4 has been released ... I'll update to that and see if that fixes the Windows linking issues. Oddly enough, it links for me locally, so I don't know what's wrong yet. But I was pinging you to see if you had any comments about any part of it.

Pat-Lafon commented 9 months ago

FWIW I tried building z3 using github actions with 4.12.4 and still ran into this issue. https://github.com/Pat-Lafon/z3.rs/actions/runs/7215253276/job/19659127883?pr=2

Pat-Lafon commented 9 months ago

I was trying a couple different commits and I think I narrowed down the issue to this commit: https://github.com/Z3Prover/z3/commit/9d3fef3e2bdf6d1806aa9c2b171b1bb6f9d41d2f . The previous commit in the history seems to pass but upgrading to a more recent cmake probably needs something else on windows.

waywardmonkeys commented 9 months ago

Look who did that commit!

It must be a cmake policy thing ... but I'm about to prepare for travel and fly half way around the world this weekend ...