按照如下链接进行 SMTChecker 验证的时候，报如下提示，需要如何解决？ https://learnblockchain.cn/article/3016

❯ solc contracts/LazyCounter.sol --model-checker-engine chc --model-checker-show-unproved Warning: CHC: Assertion violation might happen here. --> contracts/LazyCounter.sol:32:9: | 32 | assert(x >= 0 && x < 8 && y >= 0 && y < 8); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.