fn check_equality()

in z3tracer/src/model.rs [731:746]


    fn check_equality(&mut self, id1: &Ident, id2: &Ident) -> Option<usize> {
        let c1 = self.term_equality_class(id1);
        let c2 = self.term_equality_class(id2);
        if c1 != c2 {
            println!(
                "{}: @{} {:?} -> {:?} =/= {:?} <- {:?}",
                self.processed_logs, self.current_scope.level, id1, c1, c2, id2
            );
            return None;
        }
        let index = std::cmp::max(
            self.term_max_scope_index(id1),
            self.term_max_scope_index(id2),
        );
        Some(index)
    }