SMTChecker: Incorrect treatment of overflow in unary minus

## Description

SMTChecker treats unary minus incorrectly.
It reports overflow in an unchecked block, where it should not be creating overflow verification targets. This is false positive.

It also does not report overflow in a checked block, where an overflow (and subsequent revert) is possible). This is false negative.

Only unary minus is effected. Other arithmetic operations work as expected.
The problem occurs both with BMC and CHC engine.

## Steps to Reproduce

```solidity
pragma solidity ^0.8.13;

contract C {

function checkedNegMin(int8 x) external pure returns (int8) {
int8 y = -x; // overflow should be reported here
return y;
}

function uncheckedNeg(int8 x) external pure returns (int8) {
unchecked {
int8 y = -x; // overflow should not be reported in unchecked block
return y;
}
}
}
```