As a future work, we could propagate the LIA solver here and check, if the formula subst_var < 100 is valid. In that case we have a precise solution and we could set res_precision to PRECISE.

subst_var is a string var, so we would have to check something else, probably you meant |subst_var| < 3.
But I am not sure if it would work.
I was thinking about doing something a bit similar, returning multiple formulae (one underapproximation, one something like overapproximation), but it is quite complicated and it is not that clear how it should work.

Anyway, for stringfuzz, the best thing would be to transform n = str.to_int(x) on the input to n = str.to_int(x) & x ∈ 0*n (and also do that for lenghts, i.e. n = str.len(x) & x ∈ .{n}), I think that would solve everything.
So doing something with overapproximation or something similar would only be helpful for full_str_int, and it is questionable how helpful.

1. ok, and what about the same checking for from_int? Is it possible at all in our setting? The replacement of from_int by to_int is done in relevant_eh, right ?
2. Agree, there is a good hope that this can be done in seq rewriter.

1. I do not understand the question. What do you mean by same checking? Also from_int is not replaced with to_int, I do handle them in similar way during the LIA formula creation, but it is still important to know if I have to_int or from_int (for handling invalid cases).

Sorry, I wrote it confusedly. I though that the current problem (mainly for full_str_int) are constraints of the form w = from_int(x) where x is some integer variable. Because we do not know about the possible values of x, we are not currently able to solve it, right? But if we find out that x is always smaller than 100, we can enumerate it quite easily.

Hmm, I think I understand now. It can probably be somehow applied for it, I'll have to think about it.

Anyway, there are only 363 formulae with from_int in full_str_int, so I don't think it's the main problem for this benchmark right now.
You can see that the underapproximation, which is useful only for SAT cases (see how number of UNSAT cases did not change at all), already helped a lot with unknowns, however, most of them moved to TO/MO, so I think we also need to focus on simplifying the formula somehow.