projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 084518d) | patch
Fix missed case of theory preprocessing (#5531)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 26 Nov 2020 03:00:13 +0000 (21:00 -0600)
committerGitHub <noreply@github.com>
Thu, 26 Nov 2020 03:00:13 +0000 (19:00 -0800)
commitd0c352ec04846353d630073e78e5b2fea92133c2
tree41255824f4f72f0eccbc7dbb2402cb46b5b9e54atree
parent084518db641e0648164bbe4461cd98b10e937dc0commit | diff
Fix missed case of theory preprocessing (#5531)

This fixes a rare case of theory preprocessing where rewriting a quantified formula would introduce a term that would not be preprocessed. This led to solution unsoundness on a branch where the relationship between expand definitions and preprocessing is modified.

This is required for updating to the new policy for expand definitions.
src/theory/theory_preprocessor.cpp diff | blob | history