Why the verifier passes an invalid test after I added a useless argument? #2608
Description
Summary of the problem
Look at this minimal example
contract TestToken {
mapping(address => int) public balances;
constructor() public{
balances[msg.sender] = 10000;
}
// both should fail, however, actually
// it fails
function crytic_assert() view public returns (bool){
return false;
}
// it passes
function crytic_assert1(int xxx) view public returns (bool){
return false;
}
}Execute manticore-verifier test.sol --contract TestToken
and it otuputs,
Transactions done: 0. States: 1, RT Coverage: 0.0%, Failing properties: 0/2
Transactions done: 1. States: 1, RT Coverage: 48.90%, Failing properties: 0/2
Transactions done: 2. States: 1, RT Coverage: 68.28%, Failing properties: 1/2
No coverage progress. Stopping exploration.
Coverage obtained 68.28%. (RT + prop)
+----------------+------------+
| Property Named | Status |
+----------------+------------+
| crytic_assert | failed (0) |
| crytic_assert1 | passed |
+----------------+------------+
Honestly, it really astonished me. Why the obvious invalid assertion passes the verifier just after I add a useless argument xxx? Can anyone explain what happens?
Manticore version
0.3.7
Python version
3.10.5
OS / Environment
LSB Version: :core-4.1-amd64:core-4.1-noarch
Distributor ID: Fedora
Description: Fedora release 35 (Thirty Five)
Release: 35
Codename: ThirtyFive
Dependencies
appdirs==1.4.4
apsw==3.36.0.post1
argcomplete==1.12.3
argh==0.26.1
asn1crypto==1.4.0
attrs==21.2.0
Automat==20.2.0
Babel==2.9.1
Beaker==1.10.0
beautifulsoup4==4.11.0
blivet==3.4.4
blivet-gui==2.3.0
Brlapi==0.8.2
cached-property==1.5.2
capstone==5.0.0rc2
cchardet==2.1.7
cffi==1.15.0
chardet==4.0.0
charset-normalizer==2.0.4
chrome-gnome-shell==0.0.0
click==8.0.1
constantly==15.1.0
coverage==5.6b1
croniter==1.3.5
cryptography==3.4.7
crytic-compile==0.2.2
css-parser==1.0.7
cupshelpers==1.0
cytoolz==0.12.0
dasbus==1.6
dbus-python==1.2.18
decorator==5.0.9
defusedxml==0.7.1
deluge==2.0.5
distro==1.6.0
dnspython==2.1.0
ecdsa==0.17.0
eth-hash==0.5.1
eth-typing==3.2.0
eth-utils==2.1.0
fedora-third-party==0.8
feedparser==6.0.6
fonttools==4.34.4
fros==1.1
future==0.18.2
GeoIP==1.3.2
Glances==3.1.4.1
gpg==1.15.1
gssapi==1.6.14
html2text==2020.1.16
html5-parser==0.4.10
html5lib==1.1
humanize==0.5.1
hyperlink==21.0.0
idna==3.2
ifaddr==0.1.7
incremental==21.3.0
iniparse==0.4
intervaltree==3.1.0
iotop==0.6
isc==2.0
jeepney==0.7.1
Jinja2==3.1.2
koji==1.29.0
langtable==0.0.58
libcomps==0.1.18
libtorrent==2.0.6
lit==13.0.0
lxml==4.6.5
Mako==1.1.4
-e git+https://github.com/trailofbits/manticore.git@35744452a2eb56a48e9b55af02d8f686758a6c76#egg=manticore
Markdown==3.3.7
MarkupSafe==2.0.0
mechanize==0.4.7
mercurial==5.9.3
msgpack==1.0.3
netifaces==0.10.6
nftables==0.1
ntplib==0.3.3
numpy==1.21.5
odfpy==1.4.1
olefile==0.46
ordered-set==4.0.1
packaging==21.3
Paste==3.5.0
pexpect==4.8.0
pid==2.2.3
Pillow==8.3.2
ply==3.11
prettytable==3.5.0
productmd==1.33
progressbar2==3.53.2
protobuf==3.20.3
psutil==5.8.0
ptyprocess==0.6.0
pwquality==1.4.4
pyasn1==0.4.8
pyasn1-modules==0.2.8
pycairo==1.20.1
pychm==0.8.6
pycparser==2.20
pycrypto==2.6.1
pycryptodomex==3.14.1
pycups==2.0.1
pycurl==7.44.1
pydbus==0.6.0
pyelftools==0.29
pyenchant==3.2.2
pyevmasm==0.2.3
pyfdt==0.3
pygame==2.1.2
pygit2==1.6.1
Pygments==2.9.0
PyGObject==3.42.0
PyHamcrest==1.9.0
pyinotify==0.9.6
pykickstart==3.34
pyOpenSSL==21.0.0
pyparsing==2.4.7
pyparted==3.12.0
PyQt5==5.15.6
PyQt5-sip==12.9.0
PyQtWebEngine==5.15.2
pysha3==1.0.2
PySocks==1.7.1
python-augeas==1.1.0
python-dateutil==2.8.1
python-meh==0.50
python-utils==2.5.6
python-xlib==0.31
pytz==2022.1
pyudev==0.22.0
pyxdg==0.27
PyYAML==6.0
regex==2022.6.2
rencode==1.0.6
requests==2.27.1
requests-file==1.5.1
requests-ftp==0.3.1
requests-gssapi==1.2.3
rlp==3.0.0
rpm==4.17.0
rpmautospec==0.2.6
safeeyes==2.1.3
scour==0.38.1
selinux==3.3
sepolicy==3.3
service-identity==21.1.0
setools==4.4.0
setproctitle==1.2.2
sgmllib3k==1.0.0
simpleaudio==1.0.4
simpleline==1.8.2
six==1.16.0
slip==0.6.4
slip.dbus==0.6.4
slither-analyzer==0.9.1
sortedcontainers==2.4.0
sos==4.2
soupsieve==2.3.1
SSSDConfig==2.7.1
systemd-python==234
Tempita==0.5.2
toolz==0.12.0
torbrowser-launcher==0.3.5
Twisted==21.7.0
typing-extensions==3.10.0.2
unicorn==2.0.1.post1
urllib3==1.26.7
wasm==1.2
wcwidth==0.2.5
webencodings==0.5.1
z3-solver==4.11.2.0
zeroconf==0.36.9
zope.event==4.2.0
zope.interface==5.4.0
Step to reproduce the behavior
Has given above.
Expected behavior
The two obviously invalid assertions should be rejected.
Actual behavior
The crytic_assert1 indeed passes the check.
Any relevant logs
None.