A bunch of errors in CHC engine

[haoyang9804]

Description

1. Given a global function such as

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

or a member function such as

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

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

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;
  }
}