in z3tracer/src/model.rs [812:837]
fn check_matching_terms(
&self,
eqs: &HashSet<(Ident, Ident)>,
t1: &Term,
t2: &Term,
) -> RawResult<bool> {
use Term::*;
match (t1, t2) {
(
App {
name: n1, args: a1, ..
},
App {
name: n2, args: a2, ..
},
) if n1 == n2 && a1.len() == a2.len() => {
for i in 0..a1.len() {
if !self.check_matching_ids(eqs, &a1[i], &a2[i])? {
return Ok(false);
}
}
Ok(true)
}
_ => Ok(false),
}
}