fn make_terms_equal_at_scope()

in z3tracer/src/model.rs [674:711]

• 34 lines of code
• 4 McCabe index (conditional complexity)

    fn make_terms_equal_at_scope(
        &mut self,
        ancestor_scope_index: usize,
        id0: &Ident,
        id1: &Ident,
        ext_qi_deps: &[QiRef],
        ext_proof_deps: &[ProofRef],
    ) -> Ident {
        // Start with the current scope.
        if self.config.log_term_equalities {
            println!(
                "{}: @{}..={} {:?} == {:?}",
                self.processed_logs,
                self.scopes
                    .get(ancestor_scope_index)
                    .unwrap_or(&self.current_scope)
                    .level,
                self.current_scope.level,
                id0,
                id1,
            );
        }
        let cid = self.make_terms_equal(id0, id1, ext_qi_deps, ext_proof_deps);
        let mut parent_index = self.current_scope.parent_index;
        while let Some(index) = parent_index {
            if index < ancestor_scope_index {
                break;
            }
            // Also modify ancestor.
            std::mem::swap(&mut self.current_scope, &mut self.scopes[index]);
            self.make_terms_equal(id0, id1, ext_qi_deps, ext_proof_deps);
            // Do not consolidate scope for now.
            std::mem::swap(&mut self.current_scope, &mut self.scopes[index]);
            // Next scope index
            parent_index = self.scopes[index].parent_index;
        }
        cid
    }