Questions tagged [smtchecker]
SMTChecker is a formal verification module built into the Solidity compiler.
10 questions
1
vote
0
answers
15
views
Solidity SMTChecker SMT solvers
has anyone tried to put other SMT solvers other than Z3 for SMTChecker, please share your experience?
2
votes
2
answers
2k
views
What's the difference between a SAT Solver and a SMT solver?
I see people using SAT solvers and SMT solvers to verify that solidity code is doing what they are doing.
What is the difference between these two?
- 12.4k
2
votes
1
answer
225
views
Is the solidity built-in SMT Checker a form of symbolic execution?
See question. Is the SMT Checker in solidity a form of symbolic execution?
- 12.4k
4
votes
1
answer
790
views
What's the difference between SMT solvers and formal verification?
The question holds. What's the difference between the two? What would be an example of using these two tools on a minimal piece of solidity code?
- 12.4k
0
votes
1
answer
66
views
How do I know when the Solidity SMTChecker did not find any unproven targets?
From the docs:
If there are any unproved targets, the SMTChecker issues one warning stating how many unproved targets there are.
However, the docs don't say anything about the converse, i.e. what ...
- 18.7k
2
votes
0
answers
67
views
How to get the abstract model in smtlib2 format or z3 expressions from Solidity SMTChecker?
I want to get the abstract model in smtlib2 format or as Z3 expressions created by the SMTChecker. However, i cannot find any compiler switch or something to get the model. The SMTChecker ...
- 21
0
votes
1
answer
149
views
SMTChecker error with CHC
I am trying to run the SMTChecker on a contract. When I run it with the BMC checker, it runs fine, although it's pretty hard to figure out how the checker landed on a given state.
I hence wanted to ...
0
votes
1
answer
297
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 ...
- 101
2
votes
1
answer
124
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 ...
8
votes
1
answer
2k
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 ...
- 18.7k