mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-13 20:35:39 +00:00
Code Activity

Fix off-by-one column after comment lines in SMT2 scanner (#9808)

Browse source 
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>
This commit is contained in:
Lev Nachmanson 2026-06-10 06:49:31 -07:00 • committed by GitHub
parent e093be8b60
commit 1b2ca1a1bf
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/parsers/smt2/smt2scanner.cpp
View file

@ -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();