Fix missing const equality in some cases (#90)

viperproject · Dec 17, 2024 · 47a1928 · 47a1928
1 parent fa92ce2
commit 47a1928
Showing 1 changed file with 8 additions and 9 deletions.
diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/explain.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/explain.rs
@@ -427,6 +427,13 @@ impl MlExplainer {
                     self.ancestor_is_recurring = false;
                 }
                 self.ancestor_is_recurring = ancestor_is_recurring;
+                if self.ancestor_is_recurring && !self.add_mode {
+                    self.burned_eqs.insert(eq);
+                    self.add_mode = true;
+                    self.super_walk_trans(eq, forward)?;
+                    self.add_mode = false;
+                    assert!(self.ancestor_is_recurring);
+                }
                 Ok(())
             }
             fn walk_trans(
@@ -464,15 +471,7 @@ impl MlExplainer {
                     return Ok(());
                 }
 
-                self.super_walk_trans(eq, forward)?;
-                if self.ancestor_is_recurring {
-                    self.burned_eqs.insert(eq);
-                    self.add_mode = true;
-                    self.super_walk_trans(eq, forward)?;
-                    self.add_mode = false;
-                    assert!(self.ancestor_is_recurring);
-                }
-                Ok(())
+                self.super_walk_trans(eq, forward)
             }
         }
         let mut walker = TransEqGraphWalker {