fact: Definition check_ext lres := if Lit.is_pos lres then match get_form (Lit.blit lres) with | For args => if PArray.length args =? 2 then let l1 := args.[0] in let l2 := args.[1] in if Lit.is_pos l1 && negb (Lit.is_pos l2) then match get_form (Lit.blit l1), get_form (Lit.blit l2) with | Fatom eqa, Fatom eqsel => match get_atom eqa, get_atom eqsel with | Abop (BO_eq (Typ.TFArray ti te)) a b, Abop (BO_eq te') sela selb => if Typ.eqb te te' && (eq_sel_sym ti te a b sela selb || eq_sel_sym ti te b a sela selb) then lres :: nil else C._true | _, _ => C._true end | _, _ => C._true end else C._true else C._true | _ => C._true end else C._true.
imports: Bool List Int63 PArray Psatz ZArith Misc State SMT_terms FArray SMT_classes