Improving pre-SMT reasoning capabilities

In the recent proofs, I have often observed the following pattern of reasoning:

1. We need C1: X <Int pow256 for a rule/simplification to fire;
2. We have C2: X <Int pow96, say, in the path constraints, so C1 holds;
3. Our simplifications aren't powerful enough to understand that C1 holds, so rule/simplification does not get applied in Booster and then (I think?) we either fall back to Kore which uses Z3 (if we're dealing with a rule) or we do nothing (if we're dealing with a simplification).

I believe that we could/should take care of these cases before they reach the SMT solver, and I would like to understand/discuss how this could be done modularly and where it should be done.

One way of doing this for this specific case would be to write simplifications in which I could tell the engine to syntactically match the path condition, rather than semantically, along the lines of:

rule A <Int B => true
  requires A <Int C
   andBool C <=Int B
  [simplification, concrete(B, C), match(C)]

where match(C) would mean 'match the path constraints syntactically to learn C, possibly also specifying which conjunct of the requires clause to use for the match (match(C, 1), for instance). In this example, we couldn't use C <=Int B anyway because both B and C are concrete, so that constraint would be fully resolved.

Start by tracing the Booster simplification path and its fallback to Kore/Z3 for rules, focusing on how path constraints are currently used before SMT solving. The issue names no files or tests, so first establish the relevant entry points and discuss where syntactic matching could fit. Done would require an agreed modular design and concrete implementation scope.