fact: Fixpoint build_clause_aux vm (cl:list _lit) {struct cl} : option (vmap * BFormula (Formula Z) isProp) := match cl with | nil => None | l::nil => build_nlit vm l | l::cl => match build_nlit vm l with | Some (vm,bf1) => match build_clause_aux vm cl with | Some (vm,bf2) => Some (vm, AND bf1 bf2) | _ => None end | None => None end end.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz