fact: Fixpoint build_congr (eqs:list (option _lit)) (l r:list int) (c:C.t) {struct eqs} := match eqs, l, r with | nil, nil, nil => c | eq::eqs, t1::l, t2::r => match eq with | None => if t1 =? t2 then build_congr eqs l r c else C._true | Some leq => let xeq := Lit.blit leq in get_eq xeq (fun t1' t2' => if ((t1 =? t1') && (t2 =? t2')) || ((t1 =? t2') && (t2 =? t1')) then build_congr eqs l r (Lit.nlit xeq :: c) else C._true) end | _, _, _ => C._true end.
imports: Bool List Int63 PArray State SMT_terms