propagate-bv-bounds assertion violation at ../src/tactic/bv/bv_bounds_tactic.cpp Line: 335

[muchang]

Hi,
For this formula:

(declare-fun a () (_ BitVec 32))
(declare-fun b () (_ BitVec 16))
(declare-fun c () (_ BitVec 16))
(declare-fun d () (_ BitVec 16))
(declare-fun t () (_ BitVec 16))
(declare-fun e () (_ BitVec 16))
(declare-fun f () (_ BitVec 16))
(assert (let ((a!1 (bvadd (bvadd a #x00000004)
                  (bvsub (bvadd (bvadd a #x00000004)
                                #x0000003d
                                ((_ zero_extend 16) c)
                                ((_ zero_extend 16) b))
                         (bvadd a #x00000004))
                  #x00000004)))
(let ((a!2 (bvadd a!1
                  (bvsub (bvadd a!1
                                #x00000035
                                ((_ zero_extend 16) t)
                                ((_ zero_extend 16) d))
                         a!1)
                  #x00000004)))
(let ((a!3 (bvadd a!2
                  (bvsub (bvadd a!2
                                #x00000046
                                ((_ zero_extend 16) f)
                                ((_ zero_extend 16) e))
                         a!2)
                  #x00000004)))
(let ((a!4 ((_ zero_extend 24)
             (ite (bvult (bvsub #xffffffff a!3) #x00000000) #x01 #x00))))
  (and (= ((_ zero_extend 16) f) #x00000000)
       (= #x00000000 (bvsub #xffffffff a!4))))))))
(check-sat)
(check-sat-using propagate-bv-bounds)

Z3 throws out an assertion violation:

Failed to verify: b.negate(b)
ASSERTION VIOLATION
File: ../src/tactic/bv/bv_bounds_tactic.cpp
Line: 335
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: 19ba294