From c8e5dd0ca5335a2a95595a5b2b313ee482a495bf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Jul 2026 17:17:27 -0700 Subject: [PATCH] TPTP: quoted numeric tokens are distinct-objects/functors, not numerals A double-quoted TPTP token such as "138" is a distinct object, and a single-quoted '138' is a functor name; neither is an arithmetic numeral. parse_name() strips the quotes, so the subsequent is_nonempty_digit_string check was converting them into Int literals (then boxed Int->U), mis-encoding distinct objects as equal numbers. Guard both numeral checks (parse_term_primary and the atomic-formula parser) with !m_last_name_quoted so only bare unquoted digit tokens become numerals. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/cmd_context/tptp_frontend.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index f0c931369c..0d5539c6d1 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -961,7 +961,7 @@ class tptp_parser { if (n == "$true") return expr_ref(m.mk_true(), m); if (n == "$false") return expr_ref(m.mk_false(), m); - if (is_nonempty_digit_string(n)) { + if (!m_last_name_quoted && is_nonempty_digit_string(n)) { return parse_numeral_from_name(n); } @@ -1416,7 +1416,7 @@ class tptp_parser { if (n == "$true") return expr_ref(m.mk_true(), m); if (n == "$false") return expr_ref(m.mk_false(), m); - if (is_nonempty_digit_string(n)) { + if (!m_last_name_quoted && is_nonempty_digit_string(n)) { return parse_numeral_from_name(n); }