Allow quantifiers within loop invariants

[ArenBabikian]

This PR adds support for quantified expressions in loop contracts. This PR depends on #5942.

We have included 3 regression tests in this PR. However, two of them are marked as KNOWNBUG due to a current limitation of quantifiers that does not allow symbolic ranges for the quantified variable when using the SAT back-end.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Merging #6012 (c3ba7e0) into develop (763f6a2) will decrease coverage by 0.65%.
The diff coverage is 100.00%.

❗ Current head c3ba7e0 differs from pull request most recent head 6993cf4. Consider uploading reports for the commit 6993cf4 to get more accurate results

@@             Coverage Diff             @@
##           develop    #6012      +/-   ##
===========================================
- Coverage    74.90%   74.24%   -0.66%     
===========================================
  Files         1447     1444       -3     
  Lines       158198   157335     -863     
===========================================
- Hits        118491   116810    -1681     
- Misses       39707    40525     +818     

Impacted Files	Coverage Δ
src/goto-instrument/code_contracts.h	94.11% <ø> (+0.36%)	⬆️
src/goto-programs/goto_convert.cpp	91.07% <ø> (-0.63%)	⬇️
src/goto-instrument/code_contracts.cpp	84.53% <100.00%> (-0.82%)	⬇️
src/goto-checker/goto_verifier.h	0.00% <0.00%> (-100.00%)	⬇️
src/goto-instrument/wmm/shared_buffers.h	0.00% <0.00%> (-95.24%)	⬇️
src/goto-checker/goto_symex_fault_localizer.cpp	0.00% <0.00%> (-82.46%)	⬇️
src/goto-instrument/wmm/shared_buffers.cpp	0.00% <0.00%> (-77.84%)	⬇️
src/goto-checker/fault_localization_provider.h	33.33% <0.00%> (-66.67%)	⬇️
...er/stop_on_fail_verifier_with_fault_localization.h	0.00% <0.00%> (-60.87%)	⬇️
src/ansi-c/literals/convert_character_literal.cpp	31.70% <0.00%> (-40.09%)	⬇️
... and 744 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update c2f711b...6993cf4. Read the comment docs.

[SaswatPadhi]

Hi @ArenBabikian,

For the KNOWNBUG test cases, could you please try the SMT backend? CPROVER SMT2 is not expected to succeed if the SAT backend does not, but we might have some luck with Z3.

• Try running CBMC with --z3 locally
• For CI, replace KNOWNBUG with CORE smt-backend broken-cprover-smt-backend

[SaswatPadhi]

Marking this as draft for now.

The failure traces look like the one from #6106, but they don't use char*. Need to take a closer look, and may be #6106 is due to some issue with contracts -> assertion/assumption translation and not char * or __CPROVER_w_ok.

[martin-cs]

This doesn't look too controversial...