From e1d04c40218a4170fcc6885762e193696d4c958e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 23 Nov 2021 23:34:25 -0600 Subject: 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. --- src/theory/trust_substitutions.h | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/theory/trust_substitutions.h') 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 d_proving; }; } // namespace theory -- cgit v1.2.3