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?

1 Answer 1


Unfortunately this happens when the underlying SMT/Horn solver issues an error via the query API. If you open an issue at https://github.com/ethereum/solidity/issues/ with the compiler/solver version I can take a look with you.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.