projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a94548b) | patch
[Parser] Fix resolution of indexed symbols (#8383)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 25 Mar 2022 23:09:13 +0000 (16:09 -0700)
committerGitHub <noreply@github.com>
Fri, 25 Mar 2022 23:09:13 +0000 (23:09 +0000)
commita139a1f0ce824fe3e2e38e70baa115150a82a3a6
treeb3fb9319fdfbcfb7b42450d532c62e8d486becddtree
parenta94548b57cb4fdd3be53d6bd016a6b8489bf8a70commit | diff
[Parser] Fix resolution of indexed symbols (#8383)

Fixes #8377. Commit 3a97480ffab492f8272ad9c7c192d04b43eeea60 changed how
we handle indexed symbols. In particular, it added the option to resolve
them later when the arguments are known. However, the condition for when
to do this resolution was incorrect: It was applied to _all_ known
indexed symbols and not only the ones that can't immediately be resolved
to a kind. This commit fixes the condition.
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/parser/issue8377-resolve-indexed.smt2 [new file with mode: 0644] blob