Implement SMT2 incremental support for arithmetic integers

[tautschnig]

Adds support for mathematical integers (__CPROVER_integer) via a new smt_integer_theory with arithmetic and comparison operators.

Fixes: #8074

• 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.
• n/a 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).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Pull request overview

Adds SMT2 incremental support for mathematical integers (__CPROVER_integer) by introducing an integer SMT sort/term and an smt_integer_theory covering arithmetic and comparison operators.

Changes:

• Introduces smt_int_sortt and smt_int_constant_termt, plus SMT2 string serialization for the new sort/term.
• Adds smt_integer_theoryt (add/sub/mul/div/mod and comparisons) and wires integer type/constant conversion in the SMT backend.
• Updates logic IDs and enables an existing regression to run with the SMT backend.

Reviewed changes

Copilot reviewed 15 out of 15 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
src/util/mathematical_types.h	Adds can_cast_type<integer_typet> to recognize ID_integer.
src/solvers/smt2_incremental/theories/smt_integer_theory.h	Declares integer arithmetic/comparison operator factories.
src/solvers/smt2_incremental/theories/smt_integer_theory.cpp	Implements integer theory identifiers, sorts, and validation.
src/solvers/smt2_incremental/smt_to_smt2_string.cpp	Prints SMT Int sort and integer constants.
src/solvers/smt2_incremental/convert_expr_to_smt.cpp	Maps integer_typet to Int, converts literals, and routes +/* to integer theory.
src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp	Constructs __CPROVER_integer values from SMT int constants.
src/solvers/smt2_incremental/ast/smt_terms.h	Adds smt_int_constant_termt.
src/solvers/smt2_incremental/ast/smt_terms.def	Registers int_constant term kind.
src/solvers/smt2_incremental/ast/smt_terms.cpp	Implements smt_int_constant_termt storage/accessors.
src/solvers/smt2_incremental/ast/smt_sorts.h	Adds smt_int_sortt.
src/solvers/smt2_incremental/ast/smt_sorts.def	Registers int sort kind.
src/solvers/smt2_incremental/ast/smt_sorts.cpp	Implements smt_int_sortt constructor.
src/solvers/smt2_incremental/ast/smt_logics.def	Adds QF_UFLIA and QF_AUFLIA logic IDs.
src/solvers/Makefile	Builds the new smt_integer_theory.cpp.
regression/cbmc/integer-assignments1/test.desc	Enables the test for the SMT backend (removes no-new-smt).

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[codecov]

Codecov Report

❌ Patch coverage is 93.05556% with 20 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.74%. Comparing base (17ab9f4) to head (5d922fa).

Files with missing lines	Patch %	Lines
...c/solvers/smt2_incremental/convert_expr_to_smt.cpp	89.47%	8 Missing ⚠️
...smt2_incremental/construct_value_expr_from_smt.cpp	0.00%	5 Missing ⚠️
unit/solvers/smt2_incremental/ast/smt_sorts.cpp	0.00%	3 Missing ⚠️
src/solvers/smt2_incremental/ast/smt_terms.cpp	71.42%	2 Missing ⚠️
...lvers/smt2_incremental/smt_response_validation.cpp	94.11%	1 Missing ⚠️
unit/solvers/smt2_incremental/ast/smt_terms.cpp	80.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8776      +/-   ##
===========================================
+ Coverage    80.72%   80.74%   +0.01%     
===========================================
  Files         1714     1716       +2     
  Lines       189915   190196     +281     
  Branches        73       73              
===========================================
+ Hits        153311   153573     +262     
- Misses       36604    36623      +19     

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

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.