[Building MIRAI] wrapper.h:1:10: fatal error: 'z3.h' file not found

[yanliu18]

Issue

Run cargo install --locked --path ./checker failed due to

failed to run custom build command for `z3-sys v0.7.1`

Caused by

process didn't exit successfully: `<PATHTOMIRAI>/target/release/build/z3-sys-1ee5d02118b012a6/build-script-build` (exit status: 101)
  --- stdout
  cargo:rerun-if-changed=build.rs
  cargo:rerun-if-changed=wrapper.h

  --- stderr
  wrapper.h:1:10: fatal error: 'z3.h' file not found
  wrapper.h:1:10: fatal error: 'z3.h' file not found, err: true
  thread 'main' panicked at 'Unable to generate bindings: ()', ~/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/build.rs:33:14
  note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
error: failed to compile `mirai v1.1.0 (<PATHTOMIRAI>/checker)`, intermediate artifacts can be found at `<PATHTOMIRAI>/target`

Steps to Reproduce

1. brew info z3

z3: stable 4.8.17 (bottled), HEAD
High-performance theorem prover
https://github.com/Z3Prover/z3
/usr/local/Cellar/z3/4.8.17 (135 files, 94.9MB) *
  Poured from bottle on 2022-06-17 at 00:26:16

2. git clone https://github.com/facebookexperimental/MIRAI.git
3. cd MIRAI
4. ./setup.sh
5. cp binaries/libz3.dylib /usr/local/lib

cp: /usr/local/lib/libz3.dylib: Permission denied

manually copy succeeded, replaced the original libz3.dylib in /usr/local/lib
6. cargo install --locked --path ./checker

Expected Behavior

Successful build of MIRAI

Actual Results

Panic

Environment

macOS Monterey v12.3.1, Intel processor.
Rust version: rustc 1.63.0-nightly (4c5f6e627 2022-05-17)

[hermanventer]

I believe this problem is already fixed on https://github.com/hermanventer/MIRAI, which should now be regarded as the source of truth for MIRAI since no-one at Meta seems interested in merging pull requests into this repo.

[garbervetsky]

@hermanventer I tried with your fork and I got the same error.

It worked for me when I added the path of z3.h.

CPATH=/usr/local/Cellar/z3/4.9.1/include/ cargo install --locked --path ./checker

[hermanventer]

Could you append a full log of a session where you follow the installation instructions and it fails?

[garbervetsky]

@hermanventer This are the steps I followed:
./setup.sh everything looks fine.

 Installed package `cargo-audit v0.17.0` (executable `cargo-audit`)
info: using existing install for 'nightly-2022-05-18-x86_64-apple-darwin'
info: override toolchain for '<folderRemoved>/MIRAI' set to 'nightly-2022-05-18-x86_64-apple-darwin'
 Installed package `cargo-audit v0.17.0` (executable `cargo-audit`)
info: using existing install for 'nightly-2022-05-18-x86_64-apple-darwin'
info: override toolchain for '/<folderRemoved>/MIRAI' set to 'nightly-2022-05-18-x86_64-apple-darwin'

  nightly-2022-05-18-x86_64-apple-darwin unchanged - rustc 1.63.0-nightly (4c5f6e627 2022-05-17)

Then:
cargo install --locked --path ./checker

  Installing mirai v1.1.0 (<folderRemoved>/MIRAI/checker)
  Updating crates.io index
  Downloaded peeking_take_while v0.1.2
....
Compiling z3-sys v0.7.1
error: failed to run custom build command for `z3-sys v0.7.1`

Caused by:
  process didn't exit successfully: `<folderRemoved>/MIRAI/target/release/build/z3-sys-1ee5d02118b012a6/build-script-build` (exit status: 101)
  --- stdout
  cargo:rerun-if-changed=build.rs
  cargo:rerun-if-changed=wrapper.h

  --- stderr
  wrapper.h:1:10: fatal error: 'z3.h' file not found
  wrapper.h:1:10: fatal error: 'z3.h' file not found, err: true
  thread 'main' panicked at 'Unable to generate bindings: ()',˜ /.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/build.rs:33:14
  note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
warning: build failed, waiting for other jobs to finish...
error: failed to compile `mirai v1.1.0 (<folderRemoved>/MIRAI/checker)`, intermediate artifacts can be found at `<folderRemoved>/MIRAI/target`
`

[hermanventer]

From InstallationGuide.md:

For macOS the binary will have to be placed somewhere where it can be found and dynamically loaded by the Rust runtime.
You'll also need the z3 header files.

On an Intel Mac, do

sudo cp binaries/libz3.dylib /usr/local/lib
sudo cp include/*.h /usr/local/include

[garbervetsky]

Makes sense. I did copied the library but not the include files because is not in the instructions :-)
Thanks @hermanventer

[ukcw]

Hi, where would I need to place the files on an ARM Mac?

[hermanventer]

This step is no longer required. You can just build MIRAI. See the current installation guide.

[ukcw]

Hi @hermanventer, I'm installing the z3 package for another project I'm working with and have the same issue as above. I need some help because the /include files are not on the PATH I believe?

[hermanventer]

Z3 is now statically linked into MIRAI, so there is no dependency or interference from any other Z3 package you may have.