fact: Definition check_atom_aux a b := match a, b with | Acop o1, Acop o2 => cop_eqb o1 o2 | Auop UO_Zopp p1, Auop UO_Zneg q => match get_atom p1 with | Auop UO_Zpos p => check_hatom p q | _ => false end | Auop UO_Zneg p, Auop UO_Zopp q1 => match get_atom q1 with | Auop UO_Zpos q => check_hatom p q | _ => false end | Auop o1 a, Auop o2 b => uop_eqb o1 o2 && check_hatom a b | Abop o1 a1 a2, Abop o2 b1 b2 => match o1, o2 with | BO_Zplus, BO_Zplus | BO_Zmult, BO_Zmult => (check_hatom a1 b1 && check_hatom a2 b2) || (check_hatom a1 b2 && check_hatom a2 b1) | BO_Zminus, BO_Zminus | BO_Zlt, BO_Zlt | BO_Zle, BO_Zle | BO_Zge, BO_Zge | BO_Zgt, BO_Zgt => check_hatom a1 b1 && check_hatom a2 b2 | BO_Zge, BO_Zle | BO_Zle, BO_Zge | BO_Zgt, BO_Zlt | BO_Zlt, BO_Zgt => check_hatom a1 b2 && check_hatom a2 b1 | BO_eq t1, BO_eq t2 => Typ.eqb t1 t2 && ((check_hatom a1 b1 && check_hatom a2 b2) || (check_hatom a1 b2 && check_hatom a2 b1)) | BO_BVand s1, BO_BVand s2 | BO_BVor s1, BO_BVor s2 => N.eqb s1 s2 && check_hatom a1 b1 && check_hatom a2 b2 | _, _ => false end | Anop o1 l1, Anop o2 l2 => match o1, o2 with | NO_distinct t1, NO_distinct t2 => Typ.eqb t1 t2 && list_beq check_hatom l1 l2 end | Aapp f1 aargs, Aapp f2 bargs =>(f1 =? f2) && list_beq check_hatom aargs bargs | _, _ => false end.
imports: List PArray Bool Int63 ZMicromega ZArith Misc State SMT_terms BVList