Add option to ignore models during solving

[sankalpgambhir]

Adding option --ignore-models, and relevant support for it in the unrolling solver.

Description (through Stainless):

--ignore-models[=true|false]          Do not request models from solvers. (default: false)
                                      Overrides and disables check-models and feeling-lucky.

As expected, models cannot be checked if we do not ask the solver for them in the first place. Since feeling-lucky also uses models during the proof-checking phase in unrolling, it is also explicitly bypassed. The same models are also used for guiding further unrolling by discovering paths to prioritize, and thus this guidance is also bypassed here while the option is turned on.

With the option on, counterexamples are replaced by (Empty Model). Example on a bolts example changed to be broken:

[info] [Warning ] /tmp/bolts/algorithms/sorting/QuickSortListOfBigInt.scala:31:21:  => INVALID
[info]                  case Nil() => Nil[BigInt]()
[info]                                ^^^^^^^^^^^^^
[info] [Warning ] Found counter-example:
[info] [Warning ]   (Empty model)

Functionality should be complete now. I have noticed no change to a slight improvement on smaller examples from bolts/algorithms, and I am continuing to do a more comprehensive check.

I am trying to see what would be reasonable tests to have for this option. Will request merging after that.

Feel free to check and comment on this!

[sankalpgambhir]

Note that with this, the problematic example in epfl-lara/stainless#1549 can be checked:

sbt:stainless-dotty> run --solvers=smt-cvc5 /tmp/Dispenser.scala --vc-cache=false --ignore-models
[info] running (fork) stainless.Main --ignore-models --solvers=smt-cvc5 /tmp/Dispenser.scala
[...] // trimmed
[info] [  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[info] [  Info  ] ║ total: 44   valid: 44   (0 from cache, 1 trivial) invalid: 0    unknown: 0    time:   13.43                                                   ║
[info] [  Info  ] ╚═══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╝

Without --ignore-models, an exception is thrown for now, as is described in the issue.

[sankalpgambhir]

(Rebased to match with main)