I make multiple SMT queries. SMT solvers work well in practice, but they are solving a problem which is between NP-Complete to Undecidable (when quantifiers are involved [1]).

Also, we are using a very hand-wavy word definition "complexity of code". This is not the complexity-theory complexity, but instead the types of operations used and the looping/control structure. (In hindsight, I should have used a different word.) So 40 lines of multiple nested loops with multiple hashes being taken and multiple dynamic dispatches over addresses, will take much much longer to analyze than 40 lines of straight line arithmetic.

My tool attempts to guess the estimated runtime midway through the analysis, but there is no real way to accurately estimate the cost upfront. That is why I was saying that if it cost ~$200 for 20-50 LoC then if you accept all caveats then under wildly simplifying assumptions the 500 LoC might take 10x-25x of that cost.

[1] https://stackoverflow.com/a/10924475