SMTChecker: Unable to accurately determine the correctness of operations following assembly code about solidity HOT 3 CLOSED

SMTChecker is currently not able to analyze inline assembly, so it is over-approximating possible behaviours. Basically it assumes that anything could have been changed.

You should see the warning

Warning: SMTChecker: 1 unsupported language feature(s). Enable the model checker option "show unsupported" to see all of them.

And if you run with --model-checker-show-unsupported, you will see more details.

Warning: Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
 --> test.sol:5:7:
  |
5 |       assembly {
  |       ^ (Relevant source part starts here and spans across multiple lines).

from solidity.

May I ask if SMTChecker will support inline assembly in the future

from solidity.

If someone will implement it then yes :)
But at the moment, there are no concrete plans regarding this feature.

from solidity.