Skip to content

Commit

Permalink
Remove troubleshooting section from README now that problem is solved
Browse files Browse the repository at this point in the history
Signed-off-by: Hernan Ponce de Leon <[email protected]>
  • Loading branch information
hernanponcedeleon committed Oct 8, 2024
1 parent fd5a67d commit 4d2c442
Showing 1 changed file with 0 additions and 12 deletions.
12 changes: 0 additions & 12 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -51,18 +51,6 @@ To build the tool run
mvn clean install -DskipTests
```

Troubleshooting
======
**MacOS ARM**

Dartagnan automatically loads native binaries for its supported SMT solvers.
However, it always loads the x86 binaries even on MacOS ARM.
This will trigger the following error when using Z3:
```
java.lang.UnsatisfiedLinkError: no libz3 in java.library.path: [/Users/***/Library/Java/Extensions, /Library/Java/Extensions, /Network/Library/Java/Extensions, /System/Library/Java/Extensions, /usr/lib/java, .]
```
A workaround here is to manually download the ARM binaries (https://github.com/Z3Prover/z3/releases/), unpack the .zip, and place the two `.dylib` files (`libz3.dylib` and `libz3java.dylib`) into one of the folders mentioned in the error message (e.g., `Library/Java/Extensions`).

Usage
======
Dartagnan comes with a user interface (not available from the docker container) where it is easy to import, export and modify both the program and the memory model and select the options for the verification engine (see below).
Expand Down

0 comments on commit 4d2c442

Please sign in to comment.