From 3d678787c58ca87a50b1c80931dacd5f8be41d75 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?George=20P=C3=AErlea?= Date: Wed, 10 Jul 2024 14:14:34 +0800 Subject: [PATCH] Fix CVC5 model comments Previously they returned `.malformed` due to the whitespace check on L194-195. --- Auto/Parser/SMTSexp.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Auto/Parser/SMTSexp.lean b/Auto/Parser/SMTSexp.lean index e65f8b3..e34becd 100644 --- a/Auto/Parser/SMTSexp.lean +++ b/Auto/Parser/SMTSexp.lean @@ -186,6 +186,7 @@ def parseSexp (s : String) (p : String.Pos) (partialResult : PartialResult) : Pa return .complete (.app final) p else pstk := pstk.modify (pstk.size - 1) (fun arr => arr.push (.app final)) + | .comment s => pstk := pstk.modify (pstk.size - 1) (fun arr => arr.push (.atom (.comment s))) | l => -- Ordinary lexicons must be separated by whitespace or parentheses match s.get? p with