use cached scanner during kprovex

[dwightguth]

No description provided.

[radumereuta]

I did some testing on regression-new, and I can't measure any time improvements.
I did notice the default scanner is not being created anymore though:

regression-new/map-symbolic-tests-haskell$ kprovex assignment-10-spec.k -v
Parse command line options                                   =  0.009s
Outer parsing [68 modules]                                   =  0.401s
  New scanner: ASSIGNMENT-10-SPEC-RULE-CELLS                 =  0.128s
Parse spec modules [1/1 rules]                               =  0.525s
Apply prover steps                                           =  0.185s
Backend                                                      =  0.638s
Cleanup                                                      =  0.045s
Total                                                        =  1.803s

Did you run any tests that indicate this is an improvement?
We also have this issue #2122 which interferes in this case.

[dwightguth]

I mean, the examples I ran, the scanner only took a couple hundred milliseconds to run, so it's not a very noticeable improvement, but it is there. It will become more meaningful if we reduce other sources of overhead, and it will also be more noticeable on larger definitions.

[dwightguth]

Any update on this? Should we merge this or just mark the related issue as complete without it?

[radumereuta]

It's not a complete fix but it's an improvement. So let's try it.