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)
}