Shepherding #1107: Fix SMT translation of integer literals

[aqjune-aws]

--- This is a verbatim copy from #1107 ---

Issue #, if available:

N/A. Found while working on leanprover/cslib#539.

Description of changes:

This fixes SMT translation of integer literals. Previously, Strata.DL.SMT.Translate.translateTerm translated .prim (.int x) as having Lean type Prop; this PR changes it to Int.

This matters for integer-valued SMT ite terms. In CSLib/Boole (Check: leanprover/cslib#539), an expression like:

if i + 1 == n then 0 else i + 1

was producing a VC elaboration error because the branch literal 0 had type Int but was expected to have type Prop.

This PR also adds a regression test covering an integer-valued SMT ite.

Checks run:

lake env lean StrataTest/DL/SMT/TranslateTests.lean
lake env lean StrataTest/DL/SMT/DenoteTests.lean
lake env lean StrataTest/DL/SMT/EncoderTests.lean
lake build Strata.DL.SMT.Translate StrataTest.DL.SMT.TranslateTests

Let me know if you have any questions!

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[aqjune-aws]

I will confirm the internal benchmark result and proceed

-> The internal benchmark didn't regress

[tautschnig]

Closing as #1107 has been merged.