[analyzer] Fix wrong comparison generation of the ranges generated by the refutation manager

The refutation manager is removing a true bug from the test in this patch.

The problem is that the following constraint:
```
(conj_$1{struct o *}) - (reg_$3<int * r>): [-9223372036854775808, 0]
```
is encoded as:
```
(and (bvuge (bvsub $1 $3) #x8000000000000000)
     (bvule (bvsub $1 $3) #x0000000000000000))
```
The issue is that unsigned comparisons (bvuge and bvule) are being generated instead of signed comparisons (bvsge and bvsle).

When generating the expressions:
```
(conj_$1{p *}) - (reg_$3<int * r>) >= -9223372036854775808
```
and
```
(conj_$1{p *}) - (reg_$3<int * r>) <= 0
```
both -9223372036854775808 and 0 are casted to pointer type and `LTy->isSignedIntegerOrEnumerationType()` in `Z3ConstraintManager::getZ3BinExpr` only checks if the type is signed, not if it's a pointer.

Reviewers: NoQ, george.karpenkov, ddcc

Subscribers: rnkovacs, NoQ, george.karpenkov, ddcc, xazax.hun, szepet, a.sidorin

Differential Revision: https://reviews.llvm.org/D48324

llvm-svn: 335926

0 files changed, 0 insertions, 0 deletions