Questions tagged [smtchecker]

SMTChecker is a formal verification module built into the Solidity compiler.

Filter by
Sorted by
Tagged with
0
votes
1answer
46 views

How to run SMTchecker without the pragma

According to documentation pragma experimental SMTchecker won't work for latest versions. It says to use --model-checker-targets "underflow,overflow". But I don't know how. I am new in this ...
2
votes
1answer
75 views

SMT Checker : Unexpected " BMC: Insufficient funds happens here"

I was using the SMT Solidity Model Checker, and I Don't understand why I have a :" BMC: Insufficient funds happens here". My code is quite simple, I just wanted to check if the Model Checker ...
6
votes
1answer
918 views

What is SMTChecker used for in Solidity?

From the solidity docs: If you use pragma experimental SMTChecker;, then you get additional safety warnings which are obtained by querying an SMT solver. The component does not yet support all ...