diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-23 23:34:25 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-24 05:34:25 +0000 |
| commit | e1d04c40218a4170fcc6885762e193696d4c958e (patch) | |
| tree | 99a9fbce7557717364392f80828c9a05a170c30a /src/theory/trust_substitutions.h | |
| parent | f6e4fecac1d16fb737a54597cfdbe31d03d2b507 (diff) | |
Fix potential for cycles in trust substitutions (#7687)
This ensures we use only the prefix of substitutions for the *first* time a formula is proven in a substitution map.
This avoids the possibility for cycles in proof generators during non-clausal simplification, where we may reprove a formula F later at a point where later substitutions depend on F.
Diffstat (limited to 'src/theory/trust_substitutions.h')
| -rw-r--r-- | src/theory/trust_substitutions.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index 2a6997d1d..cc08c870d 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -143,6 +143,8 @@ class TrustSubstitutionMap : public ProofGenerator * two substitutions but not the third when asked to prove this equality. */ NodeUIntMap d_eqtIndex; + /** Debugging, catches potential for infinite loops */ + std::unordered_set<Node> d_proving; }; } // namespace theory |