Then rather use cmbc, which does exactly that. It translates C code into SMT rules, allows assertions on symbolic variables and solves them. And note that for harder crypto problems Z3 is not the best, it's just the easiest to use.