argotorg / argotorg/solidity

Unable to invoke the Eldarica solver (SMTChecker)

Open
#14,573 4 comments 0 reactions 0 assignees View on GitHub
bug :bug: smt
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

Open the contributing 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.