diff --git a/src/comp/middle/tstate/annotate.rs b/src/comp/middle/tstate/annotate.rs
index eec390ecd945..cd820ba28857 100644
--- a/src/comp/middle/tstate/annotate.rs
+++ b/src/comp/middle/tstate/annotate.rs
@@ -91,14 +91,15 @@ fn collect_ids_decl(&@decl d, @vec[uint] res) -> () {
     }
 }
 
-fn node_ids_in_fn(&_fn f, &ident i, &def_id d, &ann a, @vec[uint] res) -> () {
+fn node_ids_in_fn(&_fn f, &span sp, &ident i, &def_id d, &ann a,
+                  @vec[uint] res) -> () {
     auto collect_ids = walk::default_visitor();
     collect_ids = rec(visit_expr_pre  = bind collect_ids_expr(_,res),
                       visit_block_pre = bind collect_ids_block(_,res),
                       visit_stmt_pre  = bind collect_ids_stmt(_,res),
                       visit_decl_pre  = bind collect_ids_decl(_,res)
                       with collect_ids);
-    walk::walk_fn(collect_ids, f, i, d, a);
+    walk::walk_fn(collect_ids, f, sp, i, d, a);
 }
 
 fn init_vecs(&crate_ctxt ccx, @vec[uint] node_ids, uint len) -> () {
@@ -108,23 +109,24 @@ fn init_vecs(&crate_ctxt ccx, @vec[uint] node_ids, uint len) -> () {
     }
 }
 
-fn visit_fn(&crate_ctxt ccx, uint num_locals, &_fn f, &ident i,
-            &def_id d, &ann a) -> () {
+fn visit_fn(&crate_ctxt ccx, uint num_locals, &_fn f,
+            &span sp, &ident i, &def_id d, &ann a) -> () {
     let vec[uint] node_ids_ = [];
     let @vec[uint] node_ids = @node_ids_;
-    node_ids_in_fn(f, i, d, a, node_ids);
+    node_ids_in_fn(f, sp, i, d, a, node_ids);
     init_vecs(ccx, node_ids, num_locals);
 }
 
-fn annotate_in_fn(&crate_ctxt ccx, &_fn f, &ident i, &def_id f_id, &ann a)
+fn annotate_in_fn(&crate_ctxt ccx, &_fn f, &span sp, &ident i,
+                  &def_id f_id, &ann a)
     -> () {
     auto f_info = get_fn_info(ccx, f_id);
-    visit_fn(ccx, num_locals(f_info), f, i, f_id, a);
+    visit_fn(ccx, num_locals(f_info), f, sp, i, f_id, a);
 }
 
 fn annotate_crate(&crate_ctxt ccx, &crate crate) -> () {
     auto do_ann = walk::default_visitor();
-    do_ann = rec(visit_fn_pre = bind annotate_in_fn(ccx,_,_,_,_)
+    do_ann = rec(visit_fn_pre = bind annotate_in_fn(ccx,_,_,_,_,_)
                  with do_ann);
     walk::walk_crate(do_ann, crate);
 }
diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs
index 48302344d079..01d07bfc212e 100644
--- a/src/comp/middle/tstate/auxiliary.rs
+++ b/src/comp/middle/tstate/auxiliary.rs
@@ -18,7 +18,6 @@ import front::ast::expr_path;
 import front::ast::ident;
 import front::ast::controlflow;
 import front::ast::ann;
-import front::ast::ts_ann;
 import front::ast::stmt;
 import front::ast::expr;
 import front::ast::block;
@@ -54,26 +53,60 @@ import tstate::ann::extend_prestate;
 import tstate::ann::extend_poststate;
 import tstate::ann::set_precondition;
 import tstate::ann::set_postcondition;
+import tstate::ann::ts_ann;
+
+import util::common::istr;
 
 /* logging funs */
 
-fn bitv_to_str(fn_info enclosing, bitv::t v) -> str {
-  auto s = "";
+fn def_id_to_str(def_id d) -> str {
+   ret (istr(d._0) + "," + istr(d._1));
+}
 
-  for each (@tup(def_id, tup(uint, ident)) p in enclosing.vars.items()) {
-    if (bitv::get(v, p._1._0)) {
-      s += " " + p._1._1 + " ";
-    }
+fn bitv_to_str(fn_ctxt fcx, bitv::t v) -> str {
+  auto s = "";
+  auto comma = false;
+
+  for each (@tup(def_id, var_info) p in fcx.enclosing.vars.items()) {
+      if (bitv::get(v, p._1.bit_num)) {
+          s += (if (comma) { ", " } else { comma = true; "" })
+               + p._1.name + " [" + fcx.ccx.tcx.sess.span_str(p._1.sp) + "]";
+      }
   }
   ret s;
 }
 
-fn log_bitv(fn_info enclosing, bitv::t v) {
-    log(bitv_to_str(enclosing, v));
+fn log_bitv(fn_ctxt fcx, bitv::t v) {
+    log(bitv_to_str(fcx, v));
 }
 
-fn log_bitv_err(fn_info enclosing, bitv::t v) {
-    log_err(bitv_to_str(enclosing, v));
+fn first_difference_string(&fn_ctxt fcx, &bitv::t expected,
+                           &bitv::t actual) -> str {
+    let str s = "";
+    auto done = false;
+    for each (@tup(def_id, var_info) p in fcx.enclosing.vars.items()) {
+        if (!done) {
+            if (bitv::get(expected, p._1.bit_num) &&
+                !bitv::get(actual, p._1.bit_num)) {
+                
+            /*
+              for fun, try either:
+              * "ret s" after the assignment to s
+              or
+              * using break here
+              */
+            s = (p._1.name + " ["
+                 + fcx.ccx.tcx.sess.span_str(p._1.sp) + "]");
+            
+            done = true;
+            }
+        }
+    }
+    ret s;
+}
+
+fn log_bitv_err(fn_ctxt fcx, bitv::t v) {
+    log_err(bitv_to_str(fcx, v));
 }
 
 fn tos (vec[uint] v) -> str {
@@ -152,8 +185,10 @@ fn print_idents(vec[ident] idents) -> () {
 /**********************************************************************/
 /* mapping from variable name (def_id is assumed to be for a local
    variable in a given function) to bit number 
-   (also remembers the ident for error-logging purposes) */
-type var_info     = tup(uint, ident);
+   (also remembers the ident and span for error-logging purposes) */
+type var_info     = rec(uint bit_num,
+                        ident name,
+                        span sp);
 type fn_info      = rec(@std::map::hashmap[def_id, var_info] vars,
                         controlflow cf);
 
diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs
index 8de90452b6dc..c3c79d68f579 100644
--- a/src/comp/middle/tstate/bitvectors.rs
+++ b/src/comp/middle/tstate/bitvectors.rs
@@ -33,7 +33,7 @@ import tstate::ann::clear_in_poststate;
              
 fn bit_num(def_id v, fn_info m) -> uint {
   assert (m.vars.contains_key(v));
-  ret m.vars.get(v)._0;
+  ret m.vars.get(v).bit_num;
 }
 
 fn promises(&poststate p, def_id v, fn_info m) -> bool {
@@ -44,14 +44,14 @@ fn promises(&poststate p, def_id v, fn_info m) -> bool {
 // return the precondition for evaluating each expr in order.
 // So, if e0's post is {x} and e1's pre is {x, y, z}, the entire
 // precondition shouldn't include x.
-fn seq_preconds(fn_info enclosing, vec[pre_and_post] pps) -> precond {
+fn seq_preconds(fn_ctxt fcx, vec[pre_and_post] pps) -> precond {
   let uint sz = len[pre_and_post](pps);
-  let uint num_vars = num_locals(enclosing);
+  let uint num_vars = num_locals(fcx.enclosing);
 
   if (sz >= 1u) {
     auto first = pps.(0);
     assert (pps_len(first) == num_vars);
-    let precond rest = seq_preconds(enclosing,
+    let precond rest = seq_preconds(fcx,
                          slice[pre_and_post](pps, 1u, sz));
     difference(rest, first.postcondition);
     auto res = clone(first.precondition);
@@ -59,11 +59,11 @@ fn seq_preconds(fn_info enclosing, vec[pre_and_post] pps) -> precond {
 
     log("seq_preconds:");
     log("first.postcondition =");
-    log_bitv(enclosing, first.postcondition);
+    log_bitv(fcx, first.postcondition);
     log("rest =");
-    log_bitv(enclosing, rest);
+    log_bitv(fcx, rest);
     log("returning");
-    log_bitv(enclosing, res);
+    log_bitv(fcx, res);
 
     ret res;
   }
@@ -118,14 +118,14 @@ fn intersect_postconds(&vec[postcond] pcs) -> postcond {
 fn gen(&fn_ctxt fcx, &ann a, def_id id) -> bool {
   log "gen";
   assert (fcx.enclosing.vars.contains_key(id));
-  let uint i = (fcx.enclosing.vars.get(id))._0;
+  let uint i = (fcx.enclosing.vars.get(id)).bit_num;
   ret set_in_postcond(i, (ann_to_ts_ann(fcx.ccx, a)).conditions);
 }
 
 fn declare_var(&fn_info enclosing, def_id id, prestate pre)
    -> prestate {
     assert (enclosing.vars.contains_key(id));
-    let uint i = (enclosing.vars.get(id))._0;
+    let uint i = (enclosing.vars.get(id)).bit_num;
     auto res = clone(pre);
     relax_prestate(i, res);
     ret res;
@@ -134,14 +134,14 @@ fn declare_var(&fn_info enclosing, def_id id, prestate pre)
 fn gen_poststate(&fn_ctxt fcx, &ann a, def_id id) -> bool {
   log "gen_poststate";
   assert (fcx.enclosing.vars.contains_key(id));
-  let uint i = (fcx.enclosing.vars.get(id))._0;
+  let uint i = (fcx.enclosing.vars.get(id)).bit_num;
   ret set_in_poststate(i, (ann_to_ts_ann(fcx.ccx, a)).states);
 }
 
 fn kill_poststate(&fn_ctxt fcx, &ann a, def_id id) -> bool {
   log "kill_poststate";
   assert (fcx.enclosing.vars.contains_key(id));
-  let uint i = (fcx.enclosing.vars.get(id))._0;
+  let uint i = (fcx.enclosing.vars.get(id)).bit_num;
   ret clear_in_poststate(i, (ann_to_ts_ann(fcx.ccx, a)).states);
 }
 
diff --git a/src/comp/middle/tstate/ck.rs b/src/comp/middle/tstate/ck.rs
index 24e8c5e3dd72..1aa7b24b47f6 100644
--- a/src/comp/middle/tstate/ck.rs
+++ b/src/comp/middle/tstate/ck.rs
@@ -53,6 +53,7 @@ import aux::stmt_to_ann;
 import aux::num_locals;
 import aux::fixed_point_states;
 import aux::bitv_to_str;
+import aux::first_difference_string;
 
 import util::common::ty_to_str;
 import util::common::log_stmt_err;
@@ -70,12 +71,14 @@ fn check_states_expr(&fn_ctxt fcx, @expr e) -> () {
 
     if (!implies(pres, prec)) {
         auto s = "";
-        s += ("Unsatisfied precondition constraint for expression:\n");
+        auto diff = first_difference_string(fcx, prec, pres);
+        s += ("Unsatisfied precondition constraint (for example, "
+              + diff + ") for expression:\n");
         s += util::common::expr_to_str(e);
         s += ("\nPrecondition:\n");
-        s += bitv_to_str(fcx.enclosing, prec);
+        s += bitv_to_str(fcx, prec);
         s += ("\nPrestate:\n");
-        s += bitv_to_str(fcx.enclosing, pres);
+        s += bitv_to_str(fcx, pres);
         fcx.ccx.tcx.sess.span_err(e.span, s);
     }
 }
@@ -96,12 +99,14 @@ fn check_states_stmt(&fn_ctxt fcx, &stmt s) -> () {
 
     if (!implies(pres, prec)) {
         auto ss = "";
-        ss += ("Unsatisfied precondition constraint for statement:\n");
+        auto diff = first_difference_string(fcx, prec, pres);
+        ss += ("Unsatisfied precondition constraint (for example, "
+              + diff + ") for statement:\n");
         ss += util::common::stmt_to_str(s);
         ss += ("\nPrecondition:\n");
-        ss += bitv_to_str(fcx.enclosing, prec);
+        ss += bitv_to_str(fcx, prec);
         ss += ("\nPrestate: \n");
-        ss += bitv_to_str(fcx.enclosing, pres);
+        ss += bitv_to_str(fcx, pres);
         fcx.ccx.tcx.sess.span_err(s.span, ss);
     }
 }
@@ -162,7 +167,8 @@ fn check_fn_states(&fn_ctxt fcx, &_fn f, &ann a) -> () {
     check_states_against_conditions(fcx, f, a);
 }
 
-fn fn_states(&crate_ctxt ccx, &_fn f, &ident i, &def_id id, &ann a) -> () {
+fn fn_states(&crate_ctxt ccx, &_fn f, &span sp, &ident i,
+             &def_id id, &ann a) -> () {
     /* Look up the var-to-bit-num map for this function */
     assert (ccx.fm.contains_key(id));
     auto f_info = ccx.fm.get(id);
@@ -171,6 +177,8 @@ fn fn_states(&crate_ctxt ccx, &_fn f, &ident i, &def_id id, &ann a) -> () {
     check_fn_states(fcx, f, a);
 }
 
+
+
 fn check_crate(ty::ctxt cx, @crate crate) -> () {
     let crate_ctxt ccx = new_crate_ctxt(cx);
 
@@ -182,14 +190,14 @@ fn check_crate(ty::ctxt cx, @crate crate) -> () {
 
     /* Compute the pre and postcondition for every subexpression */
     auto do_pre_post = walk::default_visitor();
-    do_pre_post = rec(visit_fn_pre = bind fn_pre_post(ccx,_,_,_,_)
+    do_pre_post = rec(visit_fn_pre = bind fn_pre_post(ccx,_,_,_,_,_)
                       with do_pre_post);
     walk::walk_crate(do_pre_post, *crate);
     
     /* Check the pre- and postcondition against the pre- and poststate
        for every expression */
     auto do_states = walk::default_visitor();
-    do_states = rec(visit_fn_pre = bind fn_states(ccx,_,_,_,_)
+    do_states = rec(visit_fn_pre = bind fn_states(ccx,_,_,_,_,_)
                     with do_states);
     walk::walk_crate(do_states, *crate);
 }
diff --git a/src/comp/middle/tstate/collect_locals.rs b/src/comp/middle/tstate/collect_locals.rs
index 83931ecbc553..0a8636a6044f 100644
--- a/src/comp/middle/tstate/collect_locals.rs
+++ b/src/comp/middle/tstate/collect_locals.rs
@@ -23,6 +23,7 @@ import front::ast::ident;
 import middle::walk::walk_crate;
 import middle::walk::walk_fn;
 import middle::walk::ast_visitor;
+import front::ast::span;
 
 import aux::fn_info;
 import aux::var_info;
@@ -31,39 +32,44 @@ import aux::crate_ctxt;
 import util::common::new_def_hash;
 import util::common::uistr;
 
+type identifier = rec(ident name, def_id id, span sp);
+
 fn var_is_local(def_id v, fn_info m) -> bool {
   ret (m.vars.contains_key(v));
 }
 
-fn collect_local(&@vec[tup(ident, def_id)] vars, &@decl d) -> () {
+fn collect_local(&@vec[identifier] vars, &@decl d) -> () {
     alt (d.node) {
       case (decl_local(?loc)) {
         log("collect_local: pushing " + loc.ident);
-        vec::push[tup(ident, def_id)](*vars, tup(loc.ident, loc.id));
+        vec::push[identifier](*vars, rec(name=loc.ident,
+                                         id=loc.id,
+                                         sp=d.span));
       }
       case (_) { ret; }
     }
 }
 
-fn find_locals(&_fn f, &ident i, &def_id d, &ann a)
-    -> @vec[tup(ident,def_id)] {
-  auto res = @vec::alloc[tup(ident,def_id)](0u);
+fn find_locals(&_fn f, &span sp, &ident i, &def_id d, &ann a)
+    -> @vec[identifier] {
+  auto res = @vec::alloc[identifier](0u);
   auto visitor = walk::default_visitor();
   visitor = rec(visit_decl_pre=bind collect_local(res,_) with visitor);
-  walk_fn(visitor, f, i, d, a);
+  walk_fn(visitor, f, sp, i, d, a);
   ret res;
 }
 
 
-fn add_var(def_id v, ident nm, uint next, fn_info tbl) -> uint {
+fn add_var(def_id v, span sp, ident nm, uint next, fn_info tbl) -> uint {
   log(nm + " |-> " + util::common::uistr(next));
-  tbl.vars.insert(v, tup(next,nm));
+  tbl.vars.insert(v, rec(bit_num=next, name=nm, sp=sp));
   ret (next + 1u);
 }
 
 /* builds a table mapping each local var defined in f
    to a bit number in the precondition/postcondition vectors */
-fn mk_fn_info(&crate_ctxt ccx, &_fn f, &ident f_name, &def_id f_id, &ann a)
+fn mk_fn_info(&crate_ctxt ccx, &_fn f, &span f_sp,
+              &ident f_name, &def_id f_id, &ann a)
     -> () {
     auto res = rec(vars=@new_def_hash[var_info](),
                    cf=f.decl.cf);
@@ -73,15 +79,15 @@ fn mk_fn_info(&crate_ctxt ccx, &_fn f, &ident f_name, &def_id f_id, &ann a)
     /* ignore args, which we know are initialized;
        just collect locally declared vars */
 
-    let @vec[tup(ident,def_id)] locals = find_locals(f, f_name, f_id, a);
-    for (tup(ident,def_id) p in *locals) {
-        next = add_var(p._1, p._0, next, res);
+    let @vec[identifier] locals = find_locals(f, f_sp, f_name, f_id, a);
+    for (identifier p in *locals) {
+        next = add_var(p.id, p.sp, p.name, next, res);
     }
     /* add a pseudo-entry for the function's return value
        we can safely use the function's name itself for this purpose */
-    add_var(f_id, f_name, next, res);
+    add_var(f_id, f_sp, f_name, next, res);
 
-    log(f_name + " has " + uistr(vec::len[tup(ident, def_id)](*locals))
+    log(f_name + " has " + uistr(vec::len[identifier](*locals))
             + " locals");
    
     ccx.fm.insert(f_id, res);
@@ -92,7 +98,7 @@ fn mk_fn_info(&crate_ctxt ccx, &_fn f, &ident f_name, &def_id f_id, &ann a)
    to bit number) */
 fn mk_f_to_fn_info(&crate_ctxt ccx, @crate c) -> () {
   let ast_visitor vars_visitor = walk::default_visitor();
-  vars_visitor = rec(visit_fn_pre=bind mk_fn_info(ccx,_,_,_,_)
+  vars_visitor = rec(visit_fn_pre=bind mk_fn_info(ccx,_,_,_,_,_)
                      with vars_visitor);
 
   walk_crate(vars_visitor, *c);
diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs
index 308c99ac6205..8d9e08e51a32 100644
--- a/src/comp/middle/tstate/pre_post_conditions.rs
+++ b/src/comp/middle/tstate/pre_post_conditions.rs
@@ -151,6 +151,8 @@ import util::common::log_expr_err;
 import util::common::log_block_err;
 import util::common::log_block;
 
+import front::ast::span;
+
 fn find_pre_post_mod(&_mod m) -> _mod {
     log("implement find_pre_post_mod!");
     fail;
@@ -238,7 +240,7 @@ fn find_pre_post_exprs(&fn_ctxt fcx, &vec[@expr] args, ann a) {
     auto pps = vec::map[@expr, pre_and_post](g, args);
     auto h = get_post;
 
-    set_pre_and_post(fcx.ccx, a, seq_preconds(enclosing, pps),
+    set_pre_and_post(fcx.ccx, a, seq_preconds(fcx, pps),
         union_postconds
           (nv, (vec::map[pre_and_post, postcond](h, pps))));
 }
@@ -249,8 +251,7 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@decl d, &@expr index,
     find_pre_post_block(fcx, body);
     log("222");
     auto loop_precond = declare_var(fcx.enclosing, decl_lhs(d),
-      seq_preconds(fcx.enclosing, [expr_pp(fcx.ccx, index),
-                                   block_pp(fcx.ccx, body)]));
+      seq_preconds(fcx, [expr_pp(fcx.ccx, index), block_pp(fcx.ccx, body)]));
     auto loop_postcond = intersect_postconds
         ([expr_postcond(fcx.ccx, index), block_postcond(fcx.ccx, body)]);
     set_pre_and_post(fcx.ccx, a, loop_precond, loop_postcond);
@@ -259,13 +260,18 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@decl d, &@expr index,
 fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs,
                 &ann larger_ann, &ann new_var) -> () {
   alt (ann_to_def(fcx.ccx, new_var)) {
-    case (some[def](def_local(?d_id))) {
-      find_pre_post_expr(fcx, rhs);
-      auto p = expr_pp(fcx.ccx, rhs);
-      set_pre_and_post(fcx.ccx, larger_ann,
-                       p.precondition, p.postcondition);
-      gen(fcx, larger_ann, d_id);
-    }
+      case (some[def](?d)) {
+          alt (d) {
+              case (def_local(?d_id)) {
+                  find_pre_post_expr(fcx, rhs);
+                  auto p = expr_pp(fcx.ccx, rhs);
+                  set_pre_and_post(fcx.ccx, larger_ann,
+                                   p.precondition, p.postcondition);
+                  gen(fcx, larger_ann, d_id);
+              }
+              case (_) { find_pre_post_exprs(fcx, [lhs, rhs], larger_ann); }
+          }
+      }
     case (_) { find_pre_post_exprs(fcx, [lhs, rhs], larger_ann); }
   }
 }
@@ -401,7 +407,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
             alt (maybe_alt) {
                 case (none[@expr]) {
                     log "333";
-                    auto precond_res = seq_preconds(enclosing,
+                    auto precond_res = seq_preconds(fcx,
                                          [expr_pp(fcx.ccx, antec),
                                           block_pp(fcx.ccx, conseq)]);
                     set_pre_and_post(fcx.ccx, a, precond_res,
@@ -411,17 +417,16 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
                     find_pre_post_expr(fcx, altern);
                     log "444";
                     auto precond_true_case =
-                        seq_preconds(enclosing,
-                                     [expr_pp(fcx.ccx, antec),
-                                      block_pp(fcx.ccx, conseq)]);
+                        seq_preconds(fcx, [expr_pp(fcx.ccx, antec),
+                                           block_pp(fcx.ccx, conseq)]);
                     auto postcond_true_case = union_postconds
                         (num_local_vars,
                          [expr_postcond(fcx.ccx, antec),
                           block_postcond(fcx.ccx, conseq)]);
                     log "555";
                     auto precond_false_case = seq_preconds
-                        (enclosing,
-                         [expr_pp(fcx.ccx, antec), expr_pp(fcx.ccx, altern)]);
+                        (fcx, [expr_pp(fcx.ccx, antec),
+                               expr_pp(fcx.ccx, altern)]);
                     auto postcond_false_case = union_postconds
                         (num_local_vars,
                          [expr_postcond(fcx.ccx, antec),
@@ -456,7 +461,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
             find_pre_post_block(fcx, body);
             log "666";
             set_pre_and_post(fcx.ccx, a,
-                    seq_preconds(enclosing,
+                             seq_preconds(fcx,
                                [expr_pp(fcx.ccx, test), 
                                    block_pp(fcx.ccx, body)]),
                     intersect_postconds([expr_postcond(fcx.ccx, test),
@@ -476,8 +481,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
             }
 
             log "777";
-            set_pre_and_post(fcx.ccx, a, 
-              seq_preconds(enclosing,
+            set_pre_and_post(fcx.ccx, a, seq_preconds(fcx,
                            [block_pp(fcx.ccx, body),
                             expr_pp(fcx.ccx, test)]),
               loop_postcond);
@@ -499,19 +503,17 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
             }
             auto f = bind do_an_alt(fcx, _);
             auto alt_pps = vec::map[arm, pre_and_post](f, alts);
-            fn combine_pp(pre_and_post antec, 
-                          fn_info enclosing, &pre_and_post pp,
+            fn combine_pp(pre_and_post antec, fn_ctxt fcx, &pre_and_post pp,
                           &pre_and_post next) -> pre_and_post {
                 log "777";
-                union(pp.precondition, seq_preconds(enclosing,
-                                                    [antec, next]));
+                union(pp.precondition, seq_preconds(fcx, [antec, next]));
                 intersect(pp.postcondition, next.postcondition);
                 ret pp;
             }
             auto antec_pp = pp_clone(expr_pp(fcx.ccx, e)); 
             auto e_pp  = @rec(precondition=empty_prestate(num_local_vars),
                              postcondition=false_postcond(num_local_vars));
-            auto g = bind combine_pp(antec_pp, fcx.enclosing, _, _);
+            auto g = bind combine_pp(antec_pp, fcx, _, _);
 
             auto alts_overall_pp = vec::foldl[pre_and_post, pre_and_post]
                                     (g, e_pp, alt_pps);
@@ -668,7 +670,7 @@ fn find_pre_post_block(&fn_ctxt fcx, block b) -> () {
     plus_option[pre_and_post](pps,
        option::map[@expr, pre_and_post](g, b.node.expr));
 
-    auto block_precond  = seq_preconds(fcx.enclosing, pps);
+    auto block_precond  = seq_preconds(fcx, pps);
     auto h = get_post;
     auto postconds =  vec::map[pre_and_post, postcond](h, pps);
     /* A block may be empty, so this next line ensures that the postconds
@@ -687,7 +689,8 @@ fn find_pre_post_fn(&fn_ctxt fcx, &_fn f) -> () {
     find_pre_post_block(fcx, f.body);
 }
 
-fn fn_pre_post(crate_ctxt ccx, &_fn f, &ident i, &def_id id, &ann a) -> () {
+fn fn_pre_post(crate_ctxt ccx, &_fn f, &span sp, &ident i, &def_id id,
+               &ann a) -> () {
     assert (ccx.fm.contains_key(id));
     auto fcx = rec(enclosing=ccx.fm.get(id),
                    id=id, name=i, ccx=ccx);
@@ -704,4 +707,3 @@ fn fn_pre_post(crate_ctxt ccx, &_fn f, &ident i, &def_id id, &ann a) -> () {
 // compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
 // End:
 //
-
diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs
index 6175a48972fd..10dc882166a5 100644
--- a/src/comp/middle/tstate/states.rs
+++ b/src/comp/middle/tstate/states.rs
@@ -204,8 +204,10 @@ fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@decl d,
 
 fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a) -> bool {
   alt (ann_to_def(fcx.ccx, a_new_var)) {
-    case (some[def](def_local(?d))) { ret gen_poststate(fcx, a, d); }
-    case (_) { ret false; }
+      case (some[def](def_local(?loc))) {
+          ret gen_poststate(fcx, a, loc);
+      }
+      case (_) { ret false; }
   }
 }
 
@@ -420,9 +422,9 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
         log("if:");
         log_expr(*e);
         log("new prestate:");
-        log_bitv(fcx.enclosing, pres);
+        log_bitv(fcx, pres);
         log("new poststate:");
-        log_bitv(fcx.enclosing, expr_poststate(fcx.ccx, e));
+        log_bitv(fcx, expr_poststate(fcx.ccx, e));
 
         ret changed;
     }
@@ -637,10 +639,9 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
                             log_stmt(*s);
                             log("prestate = ");
                             log(bitv::to_str(stmt_ann.states.prestate));
-                            log_bitv(fcx.enclosing, stmt_ann.states.prestate);
+                            log_bitv(fcx, stmt_ann.states.prestate);
                             log("poststate =");
-                            log_bitv(fcx.enclosing,
-                                     stmt_ann.states.poststate);
+                            log_bitv(fcx, stmt_ann.states.poststate);
                             log("changed =");
                             log(changed);
   
@@ -740,9 +741,9 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
   log("poststate = ");
   log_states(block_states(fcx.ccx, b));
   log("pres0:");
-  log_bitv(fcx.enclosing, pres0);
+  log_bitv(fcx, pres0);
   log("post:");
-  log_bitv(fcx.enclosing, post);
+  log_bitv(fcx, post);
 
   ret changed;
 }
diff --git a/src/comp/middle/walk.rs b/src/comp/middle/walk.rs
index 3580df7e3f97..a6246d288f22 100644
--- a/src/comp/middle/walk.rs
+++ b/src/comp/middle/walk.rs
@@ -4,6 +4,8 @@ import std::option;
 import std::option::some;
 import std::option::none;
 
+import front::ast::span;
+
 // FIXME: Should visit patterns as well.
 type ast_visitor =
     rec(fn () -> bool                  keep_going,
@@ -32,9 +34,9 @@ type ast_visitor =
         fn (&@ast::expr e)              visit_expr_post,
         fn (&@ast::ty t)                visit_ty_pre,
         fn (&@ast::ty t)                visit_ty_post,
-        fn (&ast::_fn f, &ast::ident name, 
+        fn (&ast::_fn f, &span sp, &ast::ident name, 
             &ast::def_id d_id, &ast::ann a)  visit_fn_pre,
-        fn (&ast::_fn f, &ast::ident name,
+        fn (&ast::_fn f, &span sp, &ast::ident name,
             &ast::def_id d_id, &ast::ann a)  visit_fn_post);
 
 fn walk_crate(&ast_visitor v, &ast::crate c) {
@@ -95,8 +97,8 @@ fn walk_item(&ast_visitor v, @ast::item i) {
             walk_ty(v, t);
             walk_expr(v, e);
         }
-        case (ast::item_fn(?i, ?f, _, ?d, ?a)) {
-            walk_fn(v, f, i, d, a);
+        case (ast::item_fn(?nm, ?f, _, ?d, ?a)) {
+            walk_fn(v, f, i.span, nm, d, a);
         }
         case (ast::item_mod(_, ?m, _)) {
             walk_mod(v, m);
@@ -120,13 +122,14 @@ fn walk_item(&ast_visitor v, @ast::item i) {
             }
             for (@ast::method m in ob.methods) {
                 v.visit_method_pre(m);
-                walk_fn(v, m.node.meth, m.node.ident, m.node.id, m.node.ann);
+                walk_fn(v, m.node.meth, m.span,
+                        m.node.ident, m.node.id, m.node.ann);
                 v.visit_method_post(m);
             }
             alt (ob.dtor) {
                 case (none[@ast::method]) {}
                 case (some[@ast::method](?m)) {
-                    walk_fn(v, m.node.meth, m.node.ident, m.node.id,
+                    walk_fn(v, m.node.meth, m.span, m.node.ident, m.node.id,
                             m.node.ann);
                 }
             }
@@ -232,13 +235,13 @@ fn walk_fn_decl(&ast_visitor v, &ast::fn_decl fd) {
     walk_ty(v, fd.output);
 }
 
-fn walk_fn(&ast_visitor v, &ast::_fn f, &ast::ident i, &ast::def_id d,
-           &ast::ann a) {
+fn walk_fn(&ast_visitor v, &ast::_fn f, &span sp, &ast::ident i,
+           &ast::def_id d, &ast::ann a) {
     if (!v.keep_going()) { ret; }
-    v.visit_fn_pre(f, i, d, a);
+    v.visit_fn_pre(f, sp, i, d, a);
     walk_fn_decl(v, f.decl);
     walk_block(v, f.body);
-    v.visit_fn_post(f, i, d, a);
+    v.visit_fn_post(f, sp, i, d, a);
 }
 
 fn walk_block(&ast_visitor v, &ast::block b) {
@@ -471,7 +474,7 @@ fn walk_expr(&ast_visitor v, @ast::expr e) {
             // Methods
             for (@ast::method m in anon_obj.methods) {
                 v.visit_method_pre(m);
-                walk_fn(v, m.node.meth, m.node.ident, 
+                walk_fn(v, m.node.meth, m.span, m.node.ident, 
                         m.node.id, m.node.ann);
                 v.visit_method_post(m);
 
@@ -495,7 +498,8 @@ fn def_visit_arm(&ast::arm a) { }
 fn def_visit_decl(&@ast::decl d) { }
 fn def_visit_expr(&@ast::expr e) { }
 fn def_visit_ty(&@ast::ty t) { }
-fn def_visit_fn(&ast::_fn f, &ast::ident i, &ast::def_id d, &ast::ann a) { }
+fn def_visit_fn(&ast::_fn f, &span sp, &ast::ident i, &ast::def_id d,
+                &ast::ann a) { }
 
 fn default_visitor() -> ast_visitor {
 
diff --git a/src/test/compile-fail/shadow.rs b/src/test/compile-fail/shadow.rs
new file mode 100644
index 000000000000..6a67108dffe2
--- /dev/null
+++ b/src/test/compile-fail/shadow.rs
@@ -0,0 +1,25 @@
+// -*- rust -*-
+// error-pattern: a \[./src/test/compile-fail/shadow.rs:11:8:11:20
+fn foo(vec[int] c) {
+  let int a = 5;
+  let vec[int] b = [];
+
+  alt (none[int]) {
+    case (some[int](_)) {
+      for (int i in c) {
+        log a;
+        auto a = 17;
+        b += [a];
+      }
+    }
+  }
+}
+
+tag t[T] {
+  none;
+  some(T);
+}
+
+fn main() {
+  foo([]);
+}