Simplify when combining string-refinement result constraints

Due to the improvements in constant prop we increasingly have constraints
that are trivially simplified, like:

if 5 >= 2 do x else y

Also because of the way these conditions are combined - the resulting
merged if gets added to all subsequent conditions and values - we end up
with expressions like this:

if 5 >= 2 then (if 5 >= 2 do x ... else y ...) else (if 5 >= 2 do x ... else y ...)

Where the size of the expression increases exponentially to the
complexity of the original if statement even if the entire conditional
is trivial to prove right/wrong. This could likely be worked out by the
SAT solver happily enough but due to the size of the resulting
expressions (I've seen ones 1.34 billion nodes deep) it never gets there
within a reasonable time-frame.

Author: JohnDumbell

src/solvers/strings/string_constraint_generator_main.cpp

@@ -416,5 +416,5 @@ string_constraint_generatort::combine_results(
 {
   const exprt return_code = maximum(result1.first, result2.first);
   merge(result2.second, std::move(result1.second));
-  return {return_code, std::move(result2.second)};
+  return {simplify_expr(return_code, ns), std::move(result2.second)};
 }