satore: fix crash rendering a bare Var in literal->tptp-string

[PratikDhanave]

Summary

The Var? branch of literal->tptp-string (satore/tptp.rkt) crashes when handed a bare variable.

[(Var? lit) (symbol->string (Var-name->symbol lit))]   ; passes the whole struct

Var-name->symbol (unification.rkt) is documented as exact-nonnegative-integer? -> symbol? and its else clause errors on anything that is not a number or symbol-variable. The Var? guard has already established lit is a Var struct, so its name must be extracted first.

Concrete failure:

(literal->tptp-string (Var 5))
; expected: "F"   (name 5 -> A,B,C,D,E,F)
; actual:   error  "Var-name->symbol: Don't know what to do with #s(Var 5)"

Fix — extract the name, matching every other caller (Vars->symbols, the tests):

[(Var? lit) (symbol->string (Var-name->symbol (Var-name lit)))]

The bug is latent in normal use because clause->tptp-string runs its input through Vars->symbols first (which turns every Var into a symbol), so the Var? branch is only reached on a direct call.

Testing

Verified by static tracing of Var-name->symbol and the Var struct accessor. Reviewers can validate via raco test satore/tests/.

[polarbe]

Dooray! 메일 발송 실패 안내 메일 발송 실패 안내 ***@***.***) 님께 보낸 메일이 전송되지 못하였습니다. 실패 사유를 확인해보세요. * 받는 사람 :  ***@***.***) * 발송 시간 :  2026-07-25T15:10:56 * 메일 제목 :  [google-deepmind/deepmind-research] satore: fix crash rendering a bare Var in literal->tptp-string (PR #740) * 실패 사유 :  받는 사람이 현재 메일 수신을 제한하고 있습니다. 이 설정은 개인 또는 조직의 메일 수신 정책에 의해 적용되었습니다. 이 메일은 발신전용으로 회신되지 않습니다. 더 궁금하신 사항은 ***@***.*** 으로 문의해 주시기 바랍니다. © Dooray!.