The Z3 SMT solver, a type of satisfiability solver used both in research and in industry, can give better performance by either improving the underlying
implementation or using domain-specific guidance. We present a way to simulate domain-specific help automatically by reducing the search space based on the model solution, and we use it to compare two implementations of Z3′s string solver – Z3str3 (weaker) and Z3-Noodler (stronger) – with and without domain-specific help. We find that Z3-Noodler sees significantly less improvement than Z3str3 because 1) the additional “helping” constraints are in fact occasionally counterproductive and 2) Z3-Noodler solves equivalent problems much faster than Z3str3, so the relative overhead of the additional constraints is more noticed.