question how can I sun BitVec

[1214465750]

from z3 import *
if __name__ == '__main__':
    m=Optimize()
    a=BitVec("a",1)
    b = BitVec("b", 1)
    c = BitVec("c", 1)
    d = BitVec("d", 1)
    e = BitVec("e", 1)
    f = Int("f")
    list=[a,b,c]
    '''for i in range(len(list)):
        list2=[Bool()]'''

    m.add(B)
    sum=BitVec("sum", 10)
    m.add(e==Sum(a,b,c,d))

how can I get e=sum(a,b,c,d)
if a=b=c=d=1 then e=4

[NikolajBjorner]

bit-vectors of size 1 can only have values 0 or 1. So e cannot be 4.