SMTChecker: fail to report underflow

## 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
```solidity
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

Start by running the provided solc 0.8.27 command against the Solidity snippet and confirm that SMTChecker with CHC and Z3 omits the underflow warning. Trace the SMTChecker path for the `uint y=x-1` expression and make the reported result include the underflow; done means the reproducer reports that arithmetic issue.

Written by the indexing model from the issue text.