SMTChecker: fail to report underflow

[Subway2023]

Environment

• Compiler version: 0.8.27
• Target EVM version (as per compiler settings): None
• Framework/IDE (e.g. Truffle or Remix): Remix
• EVM execution environment / backend / blockchain client: None
• Operating system: Linux

Steps to Reproduce

contract C {
	function dec() public returns (uint ) {
        uint  x;
        uint  y=x-1;
        return y;
    }
}

Command

solc-0827 test.sol --model-checker-ext-calls trusted --model-checker-timeout 0 --model-checker-engine chc --model-checker-solvers z3   --model-checker-show-unproved 

Warning: Source file does not specify required compiler version! Consider adding "pragma solidity ^0.8.27;"
--> test/test.sol

Warning: Function state mutability can be restricted to pure
 --> test/test.sol:2:2:
  |
2 |     function dec() public returns (uint ) {
  |     ^ (Relevant source part starts here and spans across multiple lines).

Remix

Transaction execution failed

Analyse

SMTChecker should report underflow in uint y=x-1;. So this is a false negtive