anchor.diff:    vaApp "Block" [build_code_stmts env benv stmts]
   
   (* Build codegen_success value for body of procedure Q *)
  -let build_codegen_success_stmt (env:env) (s:stmt):exp option list =
  +let build_codegen_success_stmt (q:id) (env:env) (s:stmt):exp option list =
     let rec merge (xs:exp option list) : exp option =
       match xs with
       | [] -> None
  
positive.code:     | _ -> merge xs
    in
    gather_stmts (fun _ -> merge) aux [s]
  let build_codegen_success_stmts (env:env) (stmts:stmt list):exp =
    let empty = vaApp "ttrue" [] in
    let cons el e = match e with | None -> el | Some e -> vaApp "pbool_and" [e; el] in
    let slist = List.collect (build_codegen_success_stmt env) stmts in
    List.fold cons empty (List.rev slist)
  
  // compute parameters/returns for procedures (abstract/concrete/lemma)
  
negative.code:         fret_name = None;
          fret = tPbool;
          fspecs = [];
          fbody = Some (build_codegen_success_stmts p.pname env stmts);
          fattrs =
            if benv.is_quick then
              [(Id "opaque_to_smt", []); (Id "public_decl", []); (Id "qattr", [])] @ attrs @ attr_no_verify "admit" benv.proc.pattrs
  