Check_ExprEqvInContext Contradiction from the Assumptions

[SamirDroubi]

def test_eliminate_dead_code8(golden):
    @proc
    def foo(n: size):
        a: f32
        for i in seq(n, n):
            if i < n:
                a = 1.0
    foo = eliminate_dead_code(foo, foo.find("if _ : _"))

This test generates the following query:

*******
*******
*******
assume  M(n > 0 ∧ (n ≤ i ∧ i < n) ∧ (n > 0 ∧ (n ≤ i ∧ i < n)))
to verify
i < n == True
(i_252 < n_250) == True
smtlib2
; benchmark generated from python API
(set-info :status unknown)
(declare-fun n_250 () Int)
(declare-fun i_252 () Int)
(assert
 (let (($x91 (and (< 0 n_250) (and (<= n_250 i_252) (< i_252 n_250)))))
 (and $x91 $x91)))
(assert
 (let (($x21 (< i_252 n_250)))
 (let (($x15 (= $x21 true)))
 (not $x15))))
(check-sat)


# sat = True

Which solves to true. However, we know from the assumptions that n <= i so i < n shouldn't be equal to True. There is a contradiction in the assumption itself. I am not sure if that's where the bug originates from?

This is what's currently outputted from the scheduling operation:

def foo(n: size):
    a: f32 @ DRAM
    for i in seq(n, n):
        a = 1.0

However, the output should be:

def foo(n: size):
    a: f32 @ DRAM
    for i in seq(n, n):
        pass