Solving for inverse.

[chriseth]

The main obstacle here is solving the following (low_addr is known, inverse is not):

(inverse * (low_addr - 65532) - 1) * (low_addr - 65532) = 0;

This is similar to #2619 but not exactly (maybe we can still combine both):

We try to solve both branches. The RHS just gives us a range constraint low_addr = 65532 - but low_addr was already known (not that this only works for the "only concrete known is known").

On the LHS we can only do the division if we know that low_addr - 65532 is not zero.

This is a slight problem with the new data structures, since we need to solve one branch in the "only concrete is known" version and the other branch in the "also symbolically known is known" version.

[github-actions]

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Benchmarks'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.

Benchmark suite	Current: cab979d	Previous: efdc4f1	Ratio
jit-witgen-benchmark/jit_witgen_benchmark	10619040669 ns/iter (± 75290523)	7621602996 ns/iter (± 86241071)	1.39

This comment was automatically generated by workflow using github-action-benchmark.

[chriseth]

We can probably solve in regular mode and then convert the symbolic expressions to QSEs by translating all references to unknown variables (known concrete variables will not appear anyway!)