I know Z3 is perfect for analyzing arithmetic theories. But, I'm just wondering if Z3 can also analyze String data types. Let's say we have something like this:
public void getData (String data)
String tempData = data;
I want to add this constraints to Z3 solver and get a SAT result saying that tempData = data. Is there any way to do that?