projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 89641ef) | patch
Properly printing INST_PATTERN_LIST by itself (#6507)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Fri, 7 May 2021 20:28:44 +0000 (17:28 -0300)
committerGitHub <noreply@github.com>
Fri, 7 May 2021 20:28:44 +0000 (20:28 +0000)
commitbf62473ea3bed27f13f0eb320cea404ebadb490e
tree015868df1c08327b490d60ec628b56f8cd751bbbtree
parent89641ef6aae22610cf544f1e7545178ee6418597commit | diff
Properly printing INST_PATTERN_LIST by itself (#6507)

Previously the SMT2 printer would print pattern lists wrong when they were not printed as part of a binder containing it. This commit fixes this by removing an unused hardcoded restriction that led to issues when printing the ASTs of proof nodes containing patterns.
src/printer/smt2/smt2_printer.cpp diff | blob | history