Unable to invoke the Eldarica solver (SMTChecker)
- Dominant language
- C++
- Stars
- 25.7k
- Forks
- 6.2k
- Avg merge
- 1d 11h
- Merged PRs (30d)
- 21
Description
## Description
By using solvers = [ 'eld' ] in the foundry.toml file, I get 'Warning (1218): CHC: Error trying to invoke SMT solver.' message. But eldarica is installed in my mac and accessible via the command eld in any folder.
## Environment
- Compiler version: solc 0.8.21
- Framework/IDE (e.g. Truffle or Remix): Foundry (forge 0.2.0)
- Operating system: macOS Monterey (12.6.8)
## Steps to Reproduce
Using this content in foundry.toml:
```toml
[profile.default]
src = "src"
out = "out"
libs = ["lib"]
# See more config options https://github.com/foundry-rs/foundry/tree/master/config
[profile.default.model_checker]
engine = 'chc'
solvers = [ 'eld' ]
timeout = 0
targets = [
"assert",
"constantCondition",
"divByZero",
"outOfBounds",
"overflow",
"underflow"
]
invariants = [ 'contract' ]
showProved = true
showProvedSafe = true
[profile.default.model_checker.contracts]
'src/Monotonic.sol' = [ 'Monotonic' ]
```
After running this command line 'forge build --force', I get:
```
[⠢] Compiling...
[⠒] Compiling 16 files with 0.8.21
[⠆] Solc 0.8.21 finished in 8.49s
Compiler run successful with warnings:
Warning (1218): CHC: Error trying to invoke SMT solver.
--> src/Monotonic.sol:7:16:
|
7 | return x * 42;
| ^^^^^^
Warning (1218): CHC: Error trying to invoke SMT solver.
--> src/Monotonic.sol:12:9:
|
12 | assert(f(b) > f(a));
| ^^^^^^^^^^^^^^^^^^^
Warning (5840): CHC: 2 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
```
For this example (found in SMTchecker documentation from https://docs.soliditylang.org/en/latest/smtchecker.html:
```solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity =0.8.21;
contract Monotonic {
function f(uint x) internal pure returns (uint) {
require(x < type(uint128).max);
return x * 42;
}
function inv(uint a, uint b) public pure {
require(b > a);
assert(f(b) > f(a));
}
}
```
Thanks!
Contributor guide
Research direction
Reproduce the issue with the supplied foundry.toml and src/Monotonic.sol using forge build --force. Start at the SMTChecker model-checker path that invokes the eld solver and trace why an installed eld executable is not invoked successfully. Done means the example runs without the SMT solver invocation warnings.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- solidity
- Domain
- compilers
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100