fact: Definition step_checker s (st:step) := match st with | Res pos res => S.set_resolve s pos res | Weaken pos cid cl => S.set_weaken s pos cid cl | ImmFlatten pos cid lf => S.set_clause s pos (check_flatten t_atom t_form s cid lf) | CTrue pos => S.set_clause s pos Cnf.check_True | CFalse pos => S.set_clause s pos Cnf.check_False | BuildDef pos l => S.set_clause s pos (check_BuildDef t_form l) | BuildDef2 pos l => S.set_clause s pos (check_BuildDef2 t_form l) | BuildProj pos l i => S.set_clause s pos (check_BuildProj t_form l i) | ImmBuildDef pos cid => S.set_clause s pos (check_ImmBuildDef t_form s cid) | ImmBuildDef2 pos cid => S.set_clause s pos (check_ImmBuildDef2 t_form s cid) | ImmBuildProj pos cid i => S.set_clause s pos (check_ImmBuildProj t_form s cid i) | EqTr pos l fl => S.set_clause s pos (check_trans t_form t_atom l fl) | EqCgr pos l fl => S.set_clause s pos (check_congr t_form t_atom l fl) | EqCgrP pos l1 l2 fl => S.set_clause s pos (check_congr_pred t_form t_atom l1 l2 fl) | LiaMicromega pos cl c => S.set_clause s pos (check_micromega t_form t_atom cl c) | LiaDiseq pos l => S.set_clause s pos (check_diseq t_form t_atom l) | SplArith pos orig res l => S.set_clause s pos (check_spl_arith t_form t_atom (S.get s orig) res l) | SplDistinctElim pos orig res => S.set_clause s pos (check_distinct_elim t_form t_atom (S.get s orig) res) | BBVar pos res => S.set_clause s pos (check_bbVar t_atom t_form res) | BBConst pos res => S.set_clause s pos (check_bbConst t_atom t_form res) | BBOp pos orig1 orig2 res => S.set_clause s pos (check_bbOp t_atom t_form s orig1 orig2 res) | BBNot pos orig res => S.set_clause s pos (check_bbNot t_atom t_form s orig res) | BBNeg pos orig res => S.set_clause s pos (check_bbNeg t_atom t_form s orig res) | BBAdd pos orig1 orig2 res => S.set_clause s pos (check_bbAdd t_atom t_form s orig1 orig2 res) | BBConcat pos orig1 orig2 res => S.set_clause s pos (check_bbConcat t_atom t_form s orig1 orig2 res) | BBMul pos orig1 orig2 res => S.set_clause s pos (check_bbMult t_atom t_form s orig1 orig2 res) | BBUlt pos orig1 orig2 res => S.set_clause s pos (check_bbUlt t_atom t_form s orig1 orig2 res) | BBSlt pos orig1 orig2 res => S.set_clause s pos (check_bbSlt t_atom t_form s orig1 orig2 res) | BBEq pos orig1 orig2 res => S.set_clause s pos (check_bbEq t_atom t_form s orig1 orig2 res) | BBDiseq pos res => S.set_clause s pos (check_bbDiseq t_atom t_form res) | BBExtract pos orig res => S.set_clause s pos (check_bbExtract t_atom t_form s orig res) | BBZextend pos orig res => S.set_clause s pos (check_bbZextend t_atom t_form s orig res) | BBSextend pos orig res => S.set_clause s pos (check_bbSextend t_atom t_form s orig res) | BBShl pos orig1 orig2 res => S.set_clause s pos (check_bbShl t_atom t_form s orig1 orig2 res) | BBShr pos orig1 orig2 res => S.set_clause s pos (check_bbShr t_atom t_form s orig1 orig2 res) | RowEq pos res => S.set_clause s pos (check_roweq t_form t_atom res) | RowNeq pos cl => S.set_clause s pos (check_rowneq t_form t_atom cl) | Ext pos res => S.set_clause s pos (check_ext t_form t_atom res) end.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker