how to perform symbolic-length array copy

[luca0077]

a = Array('a', BitVecSort(32),BitVecSort(8))
b = Array('b', BitVecSort(32),BitVecSort(8))

count = Concat(a0,a1,a2,a3)

now , I want simulate a memory copy instruction:
b[:count] = a[:count]

I know the below way to achieve it:

i = BitVec('i',32)
s=Solver()
constraint = ForAll(i,Implies(And(i>=0,i<count),b[i]==a[i]))
s.add(constraint)

However, what if the next I need to simulate the b[:count]=c[:count] and c is entirely different from a ?
If I use constraint(forall+implies) to perfrom array copying, then it surely will be unsat because c!=a
( b=a; b=c; means overwrite. but with "forall+implies", it's not overwrite)

and if I use " for i in range(count): Select; Store" it will also be incorrect because count is not python integer type but symbolic

So, is there any ways to resolve my problem? sincerely thanks.

(I know angr do a good job on instruction simulation. But I want do myself version)

[NikolajBjorner]

You can use "lambda" to create a new array term that behaves like a within a range and b outside the range.
Lambda(i, If(ULT(i, count), a[i], b[i]))