Lars - he/him

Here are all the files, if you'd rather not generate them, but just verify: [quant.zip](https://github.com/viperproject/silicon/files/15081548/quant.zip) For me they simply do not verify anymore starting at quant10.vpr

Awesome, thanks for looking into this! What I suspect that the complexity for the checks is quadratic since it needs to check between each pair of arrays. Thus for sufficiently...

So I have this file: After parsing takes 10minutes, it gets to the verification. On which it stack overflows eventually after approx 5 minutes. [SolveDirectionHalide-CB-P.zip](https://github.com/utwente-fmt/vercors/files/15260970/SolveDirectionHalide-CB-P.zip)

> I've added a couple flags to diagnose potential causes of parsing slowness [here](https://github.com/utwente-fmt/vercors/wiki/Parser-Analysis) > So I have this file: > > After parsing takes 10minutes, it gets to the...

ok should be ok now.

 [profile.pprof.gz](https://github.com/utwente-fmt/vercors/files/15238151/profile.pprof.gz)

If you want to make arbitrary large files that inhibit this behavior, this is the python code used to generate them: ```python base_s = """ context_everywhere n > 0; context_everywhere...

So I generated a program with 100 plusses So running intljij profiler (what an amazing app btw) it's pretty clear what function is slow:  I think this called many...

Ok bingo  when I change NumericBinExprImpl to: ```scala lazy val saved_t: Type[G] = getNumericType override def t: Type[G] = { saved_t } ``` instead of ```scala override def t:...

So running with 100 plusses can now get done within 2 minutes. Here the verification time is still trivial, but now the 'simplify' pass is pretty slow. Not sure what...