Clarify usage of history variables in error messages

[qinheping]

Resolve: #8453
loop_entry expressions are only supported in loop contracts. old expressions are only supported in function contracts. Using them in expressions in other places such as assertions may lead to conversion error.

[codecov]

Codecov Report

Attention: Patch coverage is 0% with 7 lines in your changes missing coverage. Please review.

Project coverage is 78.24%. Comparing base (2212cd6) to head (83f5c48).
Report is 8 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/solvers/smt2/smt2_conv.cpp	0.00%	7 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8456      +/-   ##
===========================================
- Coverage    78.38%   78.24%   -0.15%     
===========================================
  Files         1726     1726              
  Lines       188616   188988     +372     
  Branches     18295    18264      -31     
===========================================
+ Hits        147855   147874      +19     
- Misses       40761    41114     +353     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[tautschnig]

Can't we detect this much earlier, e.g., in the C front-end during type checking? We actually already do some such checking, I think we just need to do more of it.

[qinheping]

We can't detect this during type checking as we can't distinguish expressions in loop invariants and in __CPROVER_assert at that stage.

CBMC warned that it would ignore __CPROVER_loop_entry in assertions during prop_conv when using SAT backend. However, when using SMT backend, CBMC would throw exception without notifying that the cause is invalid usage of loop_entry.

This PR patches the case of using SMT backend and clarify the correct usage of loop_entry when exception thrown.