Your are right. I mixed up dynamic symbolic execution with invariant detection. I know there is something called DySy which does do invariant detection using dynamic symbolic execution.