argotorg / argotorg/solidity

Short circuit for `or` operator is not respected in smt checker counterexample

Open
#14,750 0 comments 0 reactions 1 assignee Claimed by @pgebal View on GitHub
bug :bug: smt
Dominant language
C++
Stars
25.7k
Forks
6.2k
Avg merge
2d 19h
Merged PRs (30d)
29

Description

in `test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol`
we have:
```
contract c {
uint x;
function f() internal returns (uint) {
x = x + 1;
return x;
}
function g() public returns (bool) {
x = 0;
bool b = (f() > 0) || (f() > 0);
assert(x == 1);
assert(!b);
return b;
}
}
```
smt checker prints the following warning
```
Warning 6328: (192-202): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n = false\nb = true\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call
```
which is invalid - function `f` is called only once, because of short circuit in `or` operator.

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.