Currently there is definitely some possibility for unsoundness if important path conditions or index conditions use expressions that we don't interpret well for z3. Usually it's not an issue, but this is something we definitely need to fix eventually.
In most cases for index expressions we just throw an error or assume something totally safe, but we need to go through the whole compiler and rethink how the abstract interpretation is set up.
Currently there is definitely some possibility for unsoundness if important path conditions or index conditions use expressions that we don't interpret well for z3. Usually it's not an issue, but this is something we definitely need to fix eventually.
In most cases for index expressions we just throw an error or assume something totally safe, but we need to go through the whole compiler and rethink how the abstract interpretation is set up.