fact: Definition check_roweq lres := if Lit.is_pos lres then match get_form (Lit.blit lres) with | Fatom a => match get_atom a with | Abop (BO_eq te) xa v => match get_atom xa with | Abop (BO_select ti1 te1) sa i => match get_atom sa with | Atop (TO_store ti2 te2) fa j v2 => if Typ.eqb ti1 ti2 && Typ.eqb te te1 && Typ.eqb te te2 && (i =? j) && (v =? v2) then lres::nil else C._true | _ => C._true end | _ => C._true end | _ => C._true end | _ => C._true end else C._true.
imports: Bool List Int63 PArray Psatz ZArith Misc State SMT_terms FArray SMT_classes