Escape SMT-LIB set-info strings per SMT-LIB 2.6+ (doubled quotes)

[tautschnig]

Verifier.encodeCore was rendering (set-info :final-message "...") with C-style escaping (backslash + quote) for embedded double quotes and backslashes in the property summary. That is invalid in SMT-LIB 2.6+: the backslash has no special meaning inside a string literal (except \u{XXXX} for Unicode escapes), so for input

Expected len(kwargs["JobName"]) >= 1, got stringLen(kwargs[JobName])

the encoder emitted

(set-info :final-message "Expected len(kwargs[\"JobName\"]) >= 1, got stringLen(kwargs[JobName])")

which an SMT-LIB parser reads as a string that ends after the first \" (a literal backslash followed by a string-closing quote), with the rest (JobName\"...) sitting outside any command and triggering a parse error. Per the spec (§3.1.2), a literal double quote inside an SMT-LIB string must be written as two consecutive double quotes.

An escapeSMTStringLit helper that already does this (and also handles non-printable characters via \u{XXXX}) existed in Strata/DDM/Util/String.lean and is already used by the user-error path in StrataMain.lean. Wire it into the Solver API as a typed setInfoString wrapper and use it everywhere a string-valued set-info attribute is emitted:

• Verifier.lean: the :final-message site (the site the reported failure hit) plus the :sat-message / :unsat-message sites in addLocationInfo. The sat-message / unsat-message callers previously pre-quoted their argument; they now pass the raw Lean string.
• SMTUtils.lean: the :file site and the forwarded application- supplied (name, value) message. The latter's contract changes from "pre-quoted value" to "raw Lean string" accordingly.

The plain setInfo remains available for attribute values that are already valid SMT-LIB tokens (integers, s-expressions), and is still used for :start / :stop.

Regression tests in SMTEncoderTests.lean cover both the reported case (embedded double quotes escaping to "") and the complementary case (embedded backslash staying literal, no escape). Each fails on origin/main and passes here.

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

[Copilot]

Pull request overview

This PR updates the SMT emission path so string-valued set-info attributes are rendered with SMT-LIB string escaping instead of C-style escaping. In the Core verifier flow, that mainly affects solver metadata such as :final-message, file/location info, and sat/unsat messages.

Changes:

• Add a typed Solver.setInfoString helper that quotes and SMT-escapes raw Lean strings.
• Switch Core verifier / imperative SMT metadata emission to use raw strings for set-info values.
• Add regression tests covering embedded quotes and literal backslashes in :final-message.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 2 comments.

File	Description
StrataTest/Languages/Core/Tests/SMTEncoderTests.lean	Adds regression coverage for :final-message escaping behavior.
Strata/Languages/Core/Verifier.lean	Updates Core SMT encoding to emit string-valued info attributes through the new helper.
Strata/DL/SMT/Solver.lean	Introduces setInfoString for SMT-LIB-safe string-valued set-info commands.
Strata/DL/Imperative/SMTUtils.lean	Switches location/info metadata emission to the new raw-string helper.

---

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

[aqjune-aws]

Indeed, escapeSMTStringLit was added from #541 and it was used if FormatOptions.smtStringEscaping was set to true, but this wasn't covering the case when String was being directly printed like this set-info case.