It doesn’t surprise me at all that bugs were found in SMT Checker. I recently wrote a blog post on how Solidity’s model checker works, and stumbled across several bugs while attempting to write simple example contracts. I didn’t even need a fuzzer :).

That area of the codebase is far from complete, which is why it is considered experimental and hidden behind a flag that you have to manually enable.