Check inferred loop assigns clauses instead of blindly trusting them

[remi-delmas-3000]

When no assigns clause is specified by the user for a loop, we infer one by inspecting assignment present in the loop body.

These inferred targets were havocked but not checked for correctness. This PR uses the inferred targets to instrument the loop as if it were user-provided.

1. In some tests the inferred assigns clause did not pass verification so an explicit assigns clause was added;
2. major performance regression on regression/contracts/quantifiers-loop-02;
3. For remaining tests, we add the assigned targets in the tests.

• 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 #6509 (ef52bb9) into develop (5f33908) will increase coverage by 0.00%.
The diff coverage is 100.00%.

@@           Coverage Diff            @@
##           develop    #6509   +/-   ##
========================================
  Coverage    75.98%   75.98%           
========================================
  Files         1578     1578           
  Lines       180910   180920   +10     
========================================
+ Hits        137467   137477   +10     
  Misses       43443    43443           

Impacted Files	Coverage Δ
src/goto-instrument/contracts/contracts.cpp	95.11% <100.00%> (+0.07%)	⬆️

---

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 e783d13...ef52bb9. Read the comment docs.

[tautschnig]

Who might be able to answer that question, or how would we find out the answer?

[feliperodri]

We should track this in a Github issue as well.

[remi-delmas-3000]

This needs careful analysis, keeping it here.

[tautschnig]

One question about the PR note:

major performance regression on regression/contracts/quantifiers-loop-02;

Can you provide more details on this?

[feliperodri]

Only minor comments.

[feliperodri]

We should track this in a Github issue as well.

[remi-delmas-3000]

One question about the PR note:

major performance regression on regression/contracts/quantifiers-loop-02;

Can you provide more details on this?

It seems that instrumenting the body of the loop adds a lot of extra complexity that the SMT backend cannot handle combined with the quantifier (arithmetic and pointer reasoning) (had to ctrl-c the analysis after 20+ minutes). I reduced the MAX_ARRAY_SIZE to make it pass.