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

`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.

---------

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

Strata/DL/Imperative/SMTUtils.lean

@@ -275,17 +275,21 @@ def solverResult {P : PureExpr} [ToFormat P.Ident]
   | none =>
     return .error (mkError output)
 
+/-- Emit a block of `set-info` attributes describing the source location and
+    an optional application-specific `(name, rawValue)` pair. `message.snd` is
+    a raw Lean string; it will be quoted and SMT-LIB-escaped (doubled `""`)
+    before emission. -/
 def addLocationInfo {P : PureExpr} [BEq P.Ident]
   (md : Imperative.MetaData P) (message : String × String)
   : Strata.SMT.SolverM Unit := do
   match Imperative.getFileRange md with
     | .some fileRange => do
-      Strata.SMT.Solver.setInfo "file" s!"\"{format fileRange.file}\""
+      Strata.SMT.Solver.setInfoString "file" (toString (format fileRange.file))
       Strata.SMT.Solver.setInfo "start" s!"{fileRange.range.start}"
       Strata.SMT.Solver.setInfo "stop" s!"{fileRange.range.stop}"
       -- TODO: the following should probably be stored in metadata so it can be
       -- set in an application-specific way.
-      Strata.SMT.Solver.setInfo message.fst message.snd
+      Strata.SMT.Solver.setInfoString message.fst message.snd
     | .none => pure ()
 
 /--

Strata/DL/SMT/Solver.lean

@@ -10,6 +10,7 @@ public import Strata.DL.SMT.Term
 public import Strata.DL.SMT.TermType
 public import Strata.Languages.Core.Options
 import Strata.DDM.Format
+public import Strata.DDM.Util.String
 import Std.Data.HashMap
 
 /-!
@@ -156,6 +157,15 @@ def setOption (name value : String) : SolverM Unit :=
 def setInfo (name value : String) : SolverM Unit :=
   emitln s!"(set-info :{name} {value})"
 
+/-- Emit `(set-info :name "...")` with the given *raw* Lean string as the
+    attribute value. The string is quoted and escaped per SMT-LIB 2.6+ rules
+    (via `Strata.escapeSMTStringLit`): embedded double quotes are doubled
+    (`""`) and non-printable characters use `\u{XXXX}` escapes. Callers must
+    NOT pre-quote or pre-escape the argument — use `setInfo` for already-
+    formatted attribute values (integers, s-expressions, etc.). -/
+def setInfoString (name value : String) : SolverM Unit :=
+  emitln s!"(set-info :{name} {Strata.escapeSMTStringLit value})"
+
 def comment (comment : String) : SolverM Unit :=
   let inline := comment.replace "\n" " "
   emitln s!"; {inline}"

Strata/Languages/Core/Verifier.lean

@@ -103,36 +103,39 @@ def encodeCore (ctx : Core.SMT.Context) (prelude : SolverM Unit)
     -- Satisfiability check: P ∧ Q satisfiable?
     Solver.comment "Satisfiability"
     Imperative.SMT.addLocationInfo (P := Core.Expression) (md := md)
-      (message := ("sat-message", s!"\"Property can be satisfied\""))
+      (message := ("sat-message", "Property can be satisfied"))
     let obligationStr ← Solver.termToSMTString obligationId
     let _ ← Solver.checkSatAssuming [obligationStr] ids
 
     -- Validity check: P ∧ ¬Q satisfiable?
     Solver.comment "Validity"
     Imperative.SMT.addLocationInfo (P := Core.Expression) (md := md)
-      (message := ("unsat-message", s!"\"Property is always true\""))
+      (message := ("unsat-message", "Property is always true"))
     let negObligationStr := s!"(not {obligationStr})"
     let _ ← Solver.checkSatAssuming [negObligationStr] ids
   else
     if satisfiabilityCheck then
       -- P ∧ Q satisfiable?
       Solver.comment "Satisfiability"
       Imperative.SMT.addLocationInfo (P := Core.Expression) (md := md)
-        (message := ("sat-message", s!"\"Property can be satisfied\""))
+        (message := ("sat-message", "Property can be satisfied"))
       Solver.assert obligationId
       let _ ← Solver.checkSat ids
     else if validityCheck then
       -- P ∧ ¬Q satisfiable?
       Solver.comment "Validity"
       Imperative.SMT.addLocationInfo (P := Core.Expression) (md := md)
-        (message := ("unsat-message", s!"\"Property is always true\""))
+        (message := ("unsat-message", "Property is always true"))
       Solver.assert (← encodeTerm (Factory.not obligationTerm) |>.run estate).1
       let _ ← Solver.checkSat ids
 
   -- Emit the property summary (or label) as the final message in the SMT-LIB output.
+  -- Use `setInfoString` so the value is quoted and escaped per SMT-LIB 2.6+
+  -- (doubled `""` for embedded quotes). C-style `\"` escaping would be rejected
+  -- by SMT-LIB consumers: backslash is a literal character in string contexts,
+  -- and the following `"` would close the string.
   let rawMsg := md.getPropertySummary.getD label
-  let escaped := rawMsg.replace "\\" "\\\\" |>.replace "\"" "\\\""
-  Solver.setInfo "final-message" s!"\"{escaped}\""
+  Solver.setInfoString "final-message" rawMsg
 
   return (ids, estate)
 

StrataTest/Languages/Core/Tests/SMTEncoderTests.lean

@@ -370,6 +370,91 @@ info: (set-logic ALL)
     else ""
   IO.print smt
 
+/-! ## Regression: `:final-message` / `:sat-message` / `:unsat-message`
+    must escape embedded double quotes by doubling them (`""`) per
+    SMT-LIB 2.6+, not with C-style `\"` escaping.
+
+    Before the fix, a property summary containing `"` would render as
+    `(set-info :final-message "... \"FOO\" ...")` which SMT-LIB parsers
+    reject: the backslash is a literal character in string contexts, and
+    the following `"` closes the string, leaving `FOO\"...` outside as
+    unexpected tokens. See
+    https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf
+    §3.1.2. -/
+
+/-- Run `encodeCore` on a trivial `true` obligation with the given metadata
+    and check flags, and return the resulting SMT-LIB text. -/
+private def captureEncodeCore (md : Imperative.MetaData Core.Expression)
+    (satCheck validityCheck : Bool) (label : String := "test") : IO String := do
+  let ctx : SMT.Context := SMT.Context.default
+  let obligationTerm := Term.prim (.bool true)
+  let b ← IO.mkRef { : IO.FS.Stream.Buffer }
+  let solver ← Strata.SMT.Solver.bufferWriter b
+  let _ ←
+    Strata.SMT.SolverM.run solver
+      (Strata.SMT.Encoder.encodeCore ctx (pure ()) [] obligationTerm md
+        (satisfiabilityCheck := satCheck) (validityCheck := validityCheck) (label := label))
+  let contents ← b.get
+  return if h : contents.data.IsValidUTF8
+         then String.fromUTF8 contents.data h
+         else ""
+
+/-- Metadata carrying only a property summary (no file range). -/
+private def summaryMd (summary : String) : Imperative.MetaData Core.Expression :=
+  Imperative.MetaData.empty.withPropertySummary summary
+
+/-- Metadata carrying only a file range (no property summary); used to
+    exercise `addLocationInfo`. -/
+private def fileRangeMd (file : String) : Imperative.MetaData Core.Expression :=
+  let fr : Strata.FileRange := ⟨.file file, Strata.SourceRange.none⟩
+  Imperative.MetaData.empty.pushElem Imperative.MetaData.fileRange (.fileRange fr)
+
+/-! Embedded double quotes in the property summary must be doubled (`""`). -/
+/--
+info: (set-logic ALL)
+; Validity
+(assert false)
+(check-sat)
+(set-info :final-message "Expected len(kwargs[""JobName""]) >= 1, got stringLen(kwargs[JobName])")
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let smt ← captureEncodeCore
+    (summaryMd "Expected len(kwargs[\"JobName\"]) >= 1, got stringLen(kwargs[JobName])")
+    false true
+  IO.print smt
+
+/-! A backslash in the property summary is a *literal* character in SMT-LIB
+    2.6+ strings (no special meaning), so no escape is needed. -/
+/--
+info: (set-info :final-message "path/with\backslash")
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let smt ← captureEncodeCore (summaryMd "path/with\\backslash") false true
+  for line in smt.splitOn "\n" do
+    if line.startsWith "(set-info :final-message" then
+      IO.println line
+
+/-! In full-check mode (both satisfiability and validity), `addLocationInfo`
+    emits `:sat-message` and `:unsat-message`. These values must not carry
+    pre-wrapping literal quote characters — before the fix, the
+    `bothChecks` branch passed `"\"Property can be satisfied\""` which, once
+    `setInfoString` re-quoted it, rendered as `"""Property..."""` (a
+    well-formed SMT-LIB string whose content has literal leading and
+    trailing `"`). -/
+/--
+info: (set-info :sat-message "Property can be satisfied")
+(set-info :unsat-message "Property is always true")
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let smt ← captureEncodeCore (fileRangeMd "test.st") true true
+  for line in smt.splitOn "\n" do
+    if line.startsWith "(set-info :sat-message"
+        ∨ line.startsWith "(set-info :unsat-message" then
+      IO.println line
+
 /-! ## SMT encoding of str.prefixof / str.suffixof -/
 
 /--