Handle quantifiers with statement expressions

[qinheping]

This pull request addresses the issue of handling quantifiers that contain statement expressions in CBMC. This fix ensures that CBMC can correctly process and verify programs that use quantifiers with statement expressions.

Changes

• goto_clean_expr.cpp: Added logic to handle quantifiers with statement expressions. This includes:
  • A new function find_base_symbol to identify the base symbol in an expression.
  • Modifications to clean_expr to handle quantifiers with statement expressions by converting them pure expressions.
• c_typecheck_expr.cpp: Updated to allow quantifiers with statement expressions.
• Tests: Introduced new tests to verify the correct handling of quantifiers with statement expressions. These tests ensure that CBMC can process and verify programs that use such quantifiers without errors.

Motivation and Context

Statement expressions may not contain side effects, and should be accepted as quantifier bodies when they don't.
Supporting quantifiers with statement expressions enhances CBMC's capability to handle a broader range of programs, e.g., GOTO program compiled from Rust MIR model-checking/kani#3737.

• 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.