A bunch of errors in CHC engine

## Description

1. Given a global function such as
```solidity
function f(uint8 b) {
uint16 a = b;
a = a / a;
}
```
or a member function such as
```solidity
function f(uint256 b) private returns (uint256) {
b = b / b;
}
```
CHC cannot detect "divide by 0" counterexample.

2. Given a public member function in a contract such as
```solidity
contract C {
function g(uint256 b) public returns (uint256) {
return b = b / b;
}
}
```
the output of CHC contains errors, such as
```
Warning: CHC: Division by zero happens here.
Counterexample:

b = 0
= 0

Transaction trace:
C.constructor()
C.g(0)
--> test2.sol:16:16:
|
16 | return b = b / b;
| ^^^^^

```
In the above warning message given by CHC, ` = 0` is misleading.

## Environment

- Compiler version:0.8.28
- Operating system: macos

## Steps to Reproduce

Here is a reproducible test program
```solidity

function f(uint8 b) {
uint16 a = b;
a = a / a;
}

function g(uint8 b) {
b = b / b;
}

contract C {
function f(uint256 b) private returns (uint256) {
b = b / b;
}
function g(uint256 b) public returns (uint256) {
return b = b / b;
}
}
```