projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 64fc027) | patch
Fix binding of quoted symbols in `define-fun` (#7655)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 17 Nov 2021 01:31:32 +0000 (17:31 -0800)
committerGitHub <noreply@github.com>
Wed, 17 Nov 2021 01:31:32 +0000 (01:31 +0000)
commit9a8c3f60a3ff556acbd3453f367b8b86ab892362
treec77672a3453319ebf335a8f6c5fb74f541837a8etree
parent64fc027773dff00ec8d935949e938679f1e39cf6commit | diff
Fix binding of quoted symbols in `define-fun` (#7655)

Our `DefineFunctionCommand` was binding the string representation of the
function symbol including the `|` quotes instead of the symbol without
the quotes. This commit fixes the issue.
src/parser/smt2/smt2.cpp diff | blob | history
src/smt/command.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/parser/quoted-define-fun.smt2 [new file with mode: 0644] blob