Assertion violation at ../src/util/vector.h Line: 369

[muchang]

[180] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 369
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
A
[180] % cat small.smt2 
(declare-fun |b@16| () (_ BitVec 32))
(declare-fun |c@93| () (_ BitVec 8))
(declare-fun |c@94| () (_ BitVec 8))
(declare-fun |c@95| () (_ BitVec 8))
(declare-fun |b@92| () (_ BitVec 32))
(declare-fun |b@168| () (_ BitVec 32))
(declare-fun |b@1240| () (_ BitVec 32))
(declare-fun |b@33608| () (_ BitVec 32))
(assert (or (and (bvule (bvadd |b@168| #b00000111111111111111111111111111) |b@33608|) (bvult (bvadd #b00000000000000000011111100000000 (bvmul |b@33608| (_ bv4294967295 32))) #b00000000000000000000000000011111) (bvule (bvadd |b@16| #b00000000000000000000000000001010 (bvmul (_ bv4294967295 32) (bvadd |b@168| (_ bv1 32)))) |b@1240|) (bvule |b@1240| |b@92|) (= |b@92| (bvor ((_ zero_extend 24) |c@94|) (bvshl ((_ zero_extend 24) |c@94|) (_ bv8 32)))) (= |b@1240| (bvor ((_ zero_extend 24) |c@94|) (bvshl (bvor ((_ zero_extend 24) |c@95|) (bvshl (bvshl ((_ zero_extend 24) |c@93|) (_ bv1 32)) #b00000000000000000000000000000010)) (_ bv8 32)))) (bvuge #b00000000000000001000000000000000 (bvadd |b@33608| (bvmul #b00000000000000111111111111111111 |b@1240|))) (bvuge |b@92| ((_ zero_extend 24) |c@95|)) (bvuge (_ bv81900 32) |b@16|))))
(check-sat)
[181] % 

Commit: 6c9bdc9