Problem with z3 (required for SMTChecker)

[shikhar229169]

In the last lesson of the 3rd video, the Security & Auditing one (TimeStamp: 7:42:10) when I run forge build, it says:

Warning (8158): Solver z3 was selected for SMTChecker but it is not available. libz3.so.4.11 was not found.

Warning (7649): CHC analysis was not possible since no Horn solver was found and enabled. The accepted solvers for CHC are Eldarica and z3.

Even after I installed z3, it is giving the same error.

[iirekm]

+1, I did (Ubuntu 24.04):

sudo apt install libz3-4
sudo ln -s /usr/lib/x86_64-linux-gnu/libz3.so.4 /usr/local/lib/libz3.so.4.8

And still the same? How can I use SMT verification in foundry? It seems the solc provided by foundry is broken.

[iirekm]

Workaround:

• install z3 and solc provided by Ubuntu
• to foundry.toml add solc = "/usr/bin/solc"
  It seems that solc provided by foundry is badly broken

[tagupta]

Followed the below steps and it worked:

1. install z3:

For Ubuntu/Debian
sudo apt-get install z3
For macOS (Homebrew)
brew install z3
For Windows (Choco)
choco install z3

2. Add this to your foundry.toml:

[smt]
solver = "z3"  # or "eldarica"

3. Verify Installation:
   run:

z3 --version

Overall foundry.toml may look like this:

[profile.default]
src = 'src'
out = 'out'
libs = ['lib']

[fuzz]
runs = 1000

[invariant]
runs = 1000
depth = 25
fail_on_revert = false

[smt]
solver = "z3"

[profile.default.model_checker]
contracts = {'./src/CaughtWithSymbolic.sol' = ['CaughtWithSymbolic']}
engine = 'chc'
timeout = 1000
targets = ['assert']