SMT translation using linear integer or real

[Bo-Yuan-Huang]

Describe your feature request. Generate SMT formulas that use LIA or LRA for better support for CHC and other synthesis tasks.

Describe the solution you'd like An option (additional to the existing BV-based translation) to select the data type.

Additional context

• Invariants on variable/expression value, e.g., x >=0 && x <= 15 for 4-bits var x.
• Configurable translation
  1. Inline checks for overflow
  2. Report set of checks
  3. Automatic invariants suggestion
  4. Semantics-preserving translation