From 1b2ca1a1bf5cec5dc16019c5e5eb0e80774f9020 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Wed, 10 Jun 2026 06:49:31 -0700
Subject: [PATCH] Fix off-by-one column after comment lines in SMT2 scanner
 (#9808)

This bug was discovered by claude analyzing the descrepency of outputs
in https://github.com/Z3Prover/bench/discussions/2516. The benchmark was
edited - a line required stats was commented out - and this exposed the
scanner inconsistent behavior.
read_comment and read_multiline_comment handled end-of-line newlines as
new_line(); next();, the reverse of the main scan() loop's next();
new_line();. This left m_spos one higher on the line following a
comment, shifting every reported column on that line by +1 (e.g. a (pop)
error reported column 5 instead of 4 when the previous line was a
comment). Reorder both comment readers to match scan() so column numbers
are consistent regardless of whether the preceding line is a comment.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/parsers/smt2/smt2scanner.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp
index f7c44f8af..3ab95ab40 100644
--- a/src/parsers/smt2/smt2scanner.cpp
+++ b/src/parsers/smt2/smt2scanner.cpp
@@ -58,8 +58,8 @@ namespace smt2 {
             if (m_at_eof)
                 return;
             if (c == '\n') {
-                new_line();
                 next();
+                new_line();
                 return;
             }
             next();
@@ -74,8 +74,8 @@ namespace smt2 {
             if (m_at_eof)
                 return;
             if (c == '\n') {
-                new_line();
                 next();
+                new_line();
                 continue;
             }
             next();