Huge performance issue solved by tiny inlining

[Swire42]

I ran into a huge performance issue using datatypes, bitvectors, and shallow linear recursion (depth<10). minimal.txt is a (somewhat) minimal example.

As a quick introduction to the file:

• transition is a function that returns a pair: (true, XXX)
• chain_slow is a recursive functions that uses both elements of the pair.
• chain_fast is the exact same function, except that instead of using the first element of the pair, it is inlined to true.

The first assertion, using chain_fast is solved instantaneously. The second assertion, using chain_slow takes hours to solve, depending on the input list size, and eats up all the available ram.

Passing the sat.smt=true flag suggested in #6930 helps. But adding a few elements to the input list quickly overcomes that.

z3 version used: 4.13.0

Note: This example is simplified to the point that the transition function plays no role in the result. (but a huge role in terms of performance). My initial use case used all the computed values, and suffered from the same performance issue, solved by inlining the chain function (but not transition as that would have been inpractical).