fixing bug with detecting symbolic variables
improved method of getting z3 solutions