summaryrefslogtreecommitdiff
path: root/src/util/index.h
diff options
context:
space:
mode:
authorHaniel Barbosa <hanielbbarbosa@gmail.com>2021-05-07 17:28:44 -0300
committerGitHub <noreply@github.com>2021-05-07 20:28:44 +0000
commitbf62473ea3bed27f13f0eb320cea404ebadb490e (patch)
tree015868df1c08327b490d60ec628b56f8cd751bbb /src/util/index.h
parent89641ef6aae22610cf544f1e7545178ee6418597 (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.
Diffstat (limited to 'src/util/index.h')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback