Fix bug: ADT constructors do not change Map to Array when using useArrayTheory option.

[thanhnguyen-aws]

Description of changes:

Bug: When useArrayTheory is enabled, the SMT encoder correctly converts Map types to Array in variable declarations and function signatures, but it did not perform this conversion for fields inside ADT (algebraic data type) constructor declarations. This caused a type mismatch: a datatype field would be declared with type Map while the rest of the encoding used Array.

Fix: Thread the useArrayTheory flag through the datatype emission pipeline:

• lMonoTyToTermType now accepts useArrayTheory and converts Map to Array when enabled.
• datatypeConstructorsToSMT passes the flag to lMonoTyToTermType.
• SMT.Context.emitDatatypes accepts and forwards the flag.
• encodeCore in Verifier.lean passes options.useArrayTheory to emitDatatypes.

Test: Added a unit test in SMTEncoderDatatypeTest.lean that verifies a datatype with a Map-typed field emits (Array Int Int) when useArrayTheory=true and (Map Int Int) when useArrayTheory=false.

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

[thanhnguyen-aws]

@keyboardDrummer-bot Please add more PR description and add a test.

[keyboardDrummer-bot]

The PR description and tests are already in place:

• Description: Explains the bug (Map→Array conversion missing in ADT constructor fields), the fix (threading useArrayTheory through lMonoTyToTermType → datatypeConstructorsToSMT → emitDatatypes → encodeCore), and the test.
• Tests: SMTEncoderDatatypeTest.lean includes containerWithMapDatatype with two #guard_msgs tests verifying that Map becomes Array when useArrayTheory=true and stays Map when false.

Let me know if you'd like any changes to the description or additional test coverage.