Solving specific value (with a lot of irrelevant assertions)

[Notselwyn]

Hey all, the program I wrote is currently dumping a lot of assertions (including irrelevant ones) into the solver, only to solve a variable specified by a subset of the assertions.

Hence I wonder: is there a way to make Z3 algorithmically ignore the irrelevant assertions?

I know about quantifier elimination (the 'qe' tactic) to get rid of these irrelevant assertions, but this doesn't work as easy as I wished for array elements (every index needing their own variable). The alternative is to implement a feature in my complex algorithm to selectively store the assertions per variable, but this costs a lot of time to implement (also because of dynamic array indicing).