LLVM optimization breaking Gazer with --math-int

[radl97]

Describe the bug

a < 0 || b < 0 becomes BvSlt (BvOr(a,b), 0) (in C it would be (a|b) < 0), which --math-int cannot handle too well...

Haven't tested Theta, but BMC gives a bad result.

To Reproduce

tools/gazer-bmc/gazer-bmc gcd1.c --memory=havoc --math-int --trace --print-final-module=output

#include <assert.h>
int gcd(int a, int b) {
        while (b != 0) {
                int t = b;
                b = a%b;
                a = t;
        }
        return a;
}

int __VERIFIER_nondet_int(void);

int main(void) {
        int a = __VERIFIER_nondet_int();
        int b = __VERIFIER_nondet_int();
        if (a < 0) {
                return 0;
        }
        if (b < 0) {
                return 0;
        }
        assert(gcd(a,b) == gcd(b,a));
}

module output:

define dso_local i32 @main() local_unnamed_addr #0 !dbg !27 {
bb:
  call void @gazer.function.entry(metadata !27)
  %tmp = call i32 @__VERIFIER_nondet_int() #4
  call void @llvm.dbg.value(metadata i32 %tmp, metadata !31, metadata !DIExpression())
  %tmp3 = call i32 @__VERIFIER_nondet_int() #4
  call void @llvm.dbg.value(metadata i32 %tmp3, metadata !32, metadata !DIExpression())
  %tmp4 = or i32 %tmp, %tmp3, !dbg !36 ; !!!
  %tmp5 = icmp slt i32 %tmp4, 0, !dbg !36
  br i1 %tmp5, label %bb10, label %bb6, !dbg !36

bb6:
  %tmp7 = call fastcc i32 @gcd(i32 %tmp, i32 %tmp3)
  call void @gazer.function.call_returned(metadata !27)
  %tmp8 = call fastcc i32 @gcd(i32 %tmp3, i32 %tmp)
  call void @gazer.function.call_returned(metadata !27)
  %tmp9 = icmp eq i32 %tmp7, %tmp8
  br i1 %tmp9, label %bb10, label %error

bb10:
  call void @gazer.function.return_value.i32(metadata !27, i32 0)
  ret i32 0

error:
  %error_phi = phi i16 [ 2, %bb6 ]
  call void @gazer.error_code(i16 %error_phi)
  unreachable
}

BMC sets a=-1 and b=1, which should have meant a successful result (a<0, so return).

This happens only without the --no-optimize flag.

Expected behavior

LLVM shouldn't merge the two if's... a<0 || b<0 is equivalent to (a|b) < 0, but with mathematical integers, the latter does not make sense...

Version (please complete the following information):

• Tested on Gazer master branch