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 use the CHC engine which, according to documentation, provides the sequence of calls that caused a given erroneous state.
But I am getting many of this type error:
Warning: CHC: Error trying to invoke SMT solver.
--> contracts/Voting/Voting.sol:188:9:
|
188 | assert(newDelegate == getDelegate(newDelegate));
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
There is one per each assertion (I am targeting only assertions for now).
The command I am running is:
solc-macos --model-checker-targets assert --model-checker-engine chc @openzeppelin/=$(pwd)/node_modules/@openzeppelin/ --model-checker-contracts "contracts/Voting/Voting.sol:Voting" --model-checker-solvers all --model-checker-timeout 0 contracts/Voting/Voting.sol
If I set the timeout to anything different than 0, but smaller than 1000, I don't get this error, but only a Warning informing that the properties could not be proved:
Warning: CHC: 5 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
Can someone give me a hint on how to debug this?
