code: public WyalFile.Stmt.Block buildVerificationCondition(WyilFile.Decl declaration, GlobalEnvironment environment,
  			VerificationCondition vc) {
  		WyalFile.Stmt antecedent = flatten(vc.antecedent);
  		Expr consequent = vc.consequent;
  		HashSet<WyalFile.VariableDeclaration> freeVariables = new HashSet<>();
  		freeVariables(antecedent, freeVariables);
  		freeVariables(consequent, freeVariables);
  		// Determine any variable aliases as necessary.
  		Expr aliases = determineVariableAliases(environment, freeVariables);
  		// Construct the initial condition
  		WyalFile.Stmt verificationCondition = implies(and(aliases, antecedent), vc.consequent);
  		// Now, generate type information for any free variables
  		if (freeVariables.size() > 0) {
  			// This indicates there are one or more free variables in the
  			// verification condition. Hence, these must be universally
  			// quantified to ensure the vc is well=typed.
  			WyalFile.VariableDeclaration[] parameters = freeVariables
  					.toArray(new WyalFile.VariableDeclaration[freeVariables.size()]);
  			WyalFile.Stmt.Block qfBody = new WyalFile.Stmt.Block(verificationCondition);
  			verificationCondition = new WyalFile.Stmt.UniversalQuantifier(parameters, qfBody);
  		}
  		// Done
  		return new WyalFile.Stmt.Block(verificationCondition);
  	}
docs: Construct a fully typed and quantified expression for representing a
  verification condition. Aside from flattening the various components, it must
  also determine appropriate variable types, including those for aliased
  variables.
  
  @param vc
  @param environment
  @return