projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4eb2234) | patch
Ensure dependency is tracked for all substitutions (#6438)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 26 Apr 2021 15:13:50 +0000 (10:13 -0500)
committerGitHub <noreply@github.com>
Mon, 26 Apr 2021 15:13:50 +0000 (15:13 +0000)
commitc86249b35609560be783289f0720923249a4d940
tree937c0c73eeee1bd74ae9fac4158434ee05939cdetree
parent4eb2234bccf033e3758a7fb7309f51f4864cba0acommit | diff
Ensure dependency is tracked for all substitutions (#6438)

This ensures that dependencies are tracked for all inferred substitutions, even if a trusted step is added.

This is required to ensure unsat cores are sound when we use e.g. non-clausal simplification + unsat cores.
src/theory/trust_substitutions.cpp diff | blob | history
src/theory/trust_substitutions.h diff | blob | history