projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bd45dc1) | patch
Handled quoted symbols in indexed operators (#8491)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 31 Mar 2022 22:09:38 +0000 (17:09 -0500)
committerGitHub <noreply@github.com>
Thu, 31 Mar 2022 22:09:38 +0000 (22:09 +0000)
commit57e5941afc9c4b4513043920bc83c29cc56f8bad
tree654ae056b0854e1316e07bf12f938805353eadadtree
parentbd45dc19adcfb3af6270e7e2373ea27f5b206205commit | diff
Handled quoted symbols in indexed operators (#8491)

Fixes https://github.com/cvc5/cvc5/issues/8489.

The SMT-LIB standard says that symbols and quoted symbols are identical page 24: `This means for instance that abc and |abc| are the same symbol.`.  We did not parse quoted symbols in indexed operators, this fixes the issue.
src/parser/smt2/Smt2.g diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/quoted-symbols.smt2 [new file with mode: 0644] blob