diff --git a/src/comp/middle/tstate/ann.rs b/src/comp/middle/tstate/ann.rs
index d8aae77e621..882dc4a42f7 100644
--- a/src/comp/middle/tstate/ann.rs
+++ b/src/comp/middle/tstate/ann.rs
@@ -112,7 +112,7 @@ fn set_in_postcond(uint i, &pre_and_post p) -> bool {
     // sets the ith bit in p's post
     auto was_set = tritv_get(p.postcondition, i);
     tritv_set(i, p.postcondition, ttrue);
-    ret was_set == dont_care;
+    ret was_set != ttrue;
 }
 
 fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
@@ -123,7 +123,7 @@ fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
 fn set_in_poststate_(uint i, &poststate p) -> bool {
     auto was_set = tritv_get(p, i);
     tritv_set(i, p, ttrue);
-    ret was_set == dont_care;
+    ret was_set != ttrue;
 
 }
 
@@ -135,14 +135,25 @@ fn clear_in_poststate(uint i, &pre_and_post_state s) -> bool {
 fn clear_in_poststate_(uint i, &poststate s) -> bool {
     auto was_set = tritv_get(s, i);
     tritv_set(i, s, tfalse);
-    ret was_set == dont_care;
+    ret was_set != tfalse;
+}
+
+fn clear_in_prestate(uint i, &pre_and_post_state s) -> bool {
+    // sets the ith bit in p's pre
+    ret clear_in_prestate_(i, s.prestate);
+}
+
+fn clear_in_prestate_(uint i, &prestate s) -> bool {
+    auto was_set = tritv_get(s, i);
+    tritv_set(i, s, tfalse);
+    ret was_set != tfalse;
 }
 
 fn clear_in_postcond(uint i, &pre_and_post s) -> bool {
     // sets the ith bit in p's post
     auto was_set = tritv_get(s.postcondition, i);
     tritv_set(i, s.postcondition, tfalse);
-    ret was_set == dont_care;
+    ret was_set != tfalse;
 }
 
 // Sets all the bits in a's precondition to equal the
diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs
index 21934ca04b7..c7e77881e85 100644
--- a/src/comp/middle/tstate/bitvectors.rs
+++ b/src/comp/middle/tstate/bitvectors.rs
@@ -43,6 +43,7 @@
 import tstate::ann::set_in_poststate;
 import tstate::ann::set_in_poststate_;
 import tstate::ann::clear_in_poststate;
+import tstate::ann::clear_in_prestate;
 import tstate::ann::clear_in_poststate_;
 import tritv::*;
 
@@ -147,22 +148,10 @@ fn seq_preconds_go(&fn_ctxt fcx, &vec[pre_and_post] pps,
     } else { ret true_precond(num_vars); }
 }
 
-/* Gee, maybe we could use foldl or something */
-fn intersect_postconds_go(&postcond first, &vec[postcond] rest) -> postcond {
-    auto sz = vec::len[postcond](rest);
-    if (sz > 0u) {
-        auto other = rest.(0);
-        intersect(first, other);
-        intersect_postconds_go(first,
-                               slice[postcond](rest, 1u,
-                                               len[postcond](rest)));
-    }
-    ret first;
-}
-
-fn intersect_postconds(&vec[postcond] pcs) -> postcond {
-    assert (len[postcond](pcs) > 0u);
-    ret intersect_postconds_go(tritv_clone(pcs.(0)), pcs);
+fn intersect_states(&prestate p, &prestate q) -> prestate {
+    auto rslt = tritv_clone(p);
+    tritv_intersect(rslt, q);
+    ret rslt;
 }
 
 fn gen(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
@@ -219,6 +208,11 @@ fn gen_poststate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
                          node_id_to_ts_ann(fcx.ccx, id).states);
 }
 
+fn kill_prestate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
+    ret clear_in_prestate(bit_num(fcx, c),
+                           node_id_to_ts_ann(fcx.ccx, id).states);
+}
+
 fn kill_poststate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
     log "kill_poststate";
     ret clear_in_poststate(bit_num(fcx, c),
@@ -254,6 +248,16 @@ fn set_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
     ret set_in_poststate_(bit_num(fcx, rec(id=id, c=ninit(ident))), t);
 }
 
+fn clear_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
+                            &node_id parent) -> bool {
+    ret kill_poststate(fcx, parent, rec(id=id, c=ninit(ident)));
+}
+
+fn clear_in_prestate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
+                            &node_id parent) -> bool {
+    ret kill_prestate(fcx, parent, rec(id=id, c=ninit(ident)));
+}
+
 //
 // Local Variables:
 // mode: rust
diff --git a/src/comp/middle/tstate/ck.rs b/src/comp/middle/tstate/ck.rs
index a65dfbbc8c1..0c13c617c47 100644
--- a/src/comp/middle/tstate/ck.rs
+++ b/src/comp/middle/tstate/ck.rs
@@ -70,9 +70,9 @@ fn check_states_expr(&fn_ctxt fcx, &@expr e) {
     log_err("check_states_expr:");
       util::common::log_expr_err(*e);
       log_err("prec = ");
-      log_bitv_err(fcx, prec);
+      log_tritv_err(fcx, prec);
       log_err("pres = ");
-      log_bitv_err(fcx, pres);
+      log_tritv_err(fcx, pres);
     */
 
     if (!implies(pres, prec)) {
@@ -99,9 +99,9 @@ fn check_states_stmt(&fn_ctxt fcx, &@stmt s) {
       log_err("check_states_stmt:");
       log_stmt_err(*s);
       log_err("prec = ");
-      log_bitv_err(fcx, prec);
+      log_tritv_err(fcx, prec);
       log_err("pres = ");
-      log_bitv_err(fcx, pres);
+      log_tritv_err(fcx, pres);
     */
 
     if (!implies(pres, prec)) {
diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs
index 672894c0675..d4495fee622 100644
--- a/src/comp/middle/tstate/pre_post_conditions.rs
+++ b/src/comp/middle/tstate/pre_post_conditions.rs
@@ -59,7 +59,7 @@
 import bitvectors::promises;
 import bitvectors::seq_preconds;
 import bitvectors::seq_postconds;
-import bitvectors::intersect_postconds;
+import bitvectors::intersect_states;
 import bitvectors::declare_var;
 import bitvectors::gen_poststate;
 import bitvectors::relax_precond_block;
@@ -180,9 +180,8 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, &block 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)]);
+    auto loop_postcond = intersect_states(expr_postcond(fcx.ccx, index),
+                                          block_postcond(fcx.ccx, body));
     copy_pre_post_(fcx.ccx, id, loop_precond, loop_postcond);
 }
 
@@ -247,8 +246,7 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
                 seq_postconds(fcx, [precond_true_case,
                                     precond_false_case]);
             auto postcond_res =
-                intersect_postconds([postcond_true_case,
-                                     postcond_false_case]);
+                intersect_states(postcond_true_case, postcond_false_case);
             set_pre_and_post(fcx.ccx, id, precond_res, postcond_res);
         }
     }
@@ -459,10 +457,9 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
                              seq_preconds(fcx,
                                           [expr_pp(fcx.ccx, test),
                                            block_pp(fcx.ccx, body)]),
-                             intersect_postconds([expr_postcond(fcx.ccx,
-                                                                test),
-                                                  block_postcond(fcx.ccx,
-                                                                 body)]));
+                             intersect_states(expr_postcond(fcx.ccx, test),
+                                              block_postcond(fcx.ccx,
+                                                             body)));
         }
         case (expr_do_while(?body, ?test)) {
             find_pre_post_block(fcx, body);
diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs
index 0de5cf33fd4..d5676fad7ef 100644
--- a/src/comp/middle/tstate/states.rs
+++ b/src/comp/middle/tstate/states.rs
@@ -69,10 +69,12 @@
 
 import bitvectors::set_in_poststate_ident;
 import bitvectors::clear_in_poststate_expr;
-import bitvectors::intersect_postconds;
+import bitvectors::clear_in_prestate_ident;
 import bitvectors::bit_num;
 import bitvectors::gen_poststate;
 import bitvectors::kill_poststate;
+import bitvectors::clear_in_poststate_ident;
+import bitvectors::intersect_states;
 import front::ast;
 import front::ast::*;
 import middle::ty::expr_ty;
@@ -188,23 +190,27 @@ fn find_pre_post_state_exprs(&fn_ctxt fcx, &prestate pres, ast::node_id id,
 
 fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@local l,
                             &@expr index, &block body, node_id id) -> bool {
-    /* same issues as while */
+    auto loop_pres = intersect_states(pres,
+                                      block_poststate(fcx.ccx, body));
 
-    // FIXME: also want to set l as initialized, no?
-    auto changed = set_prestate_ann(fcx.ccx, id, pres) |
+    auto changed = set_prestate_ann(fcx.ccx, id, loop_pres) |
         find_pre_post_state_expr(fcx, pres, index);
-    /* in general, would need the intersection of
-       (poststate of index, poststate of body) */
         find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, index), body);
 
     if (has_nonlocal_exits(body)) { 
-        changed |= set_poststate_ann(fcx.ccx, id, pres);
+        // See [Break-unsound]
+        ret (changed | set_poststate_ann(fcx.ccx, id, pres));
     }
-
+    else {
+        auto res_p = intersect_states(expr_poststate(fcx.ccx, index),
+                                      block_poststate(fcx.ccx, body));
+    /*
     auto res_p =
         intersect_postconds([expr_poststate(fcx.ccx, index),
-                             block_poststate(fcx.ccx, body)]);
-    ret changed | set_poststate_ann(fcx.ccx, id, res_p);
+        block_poststate(fcx.ccx, body)]); */
+
+        ret changed | set_poststate_ann(fcx.ccx, id, res_p);
+    }
 }
 
 fn gen_if_local(&fn_ctxt fcx, &poststate p, &@expr e) -> bool {
@@ -269,16 +275,18 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
                 find_pre_post_state_block(fcx, conseq_prestate, conseq);
    
             auto poststate_res =
-                intersect_postconds([block_poststate(fcx.ccx, conseq),
-                                     expr_poststate(fcx.ccx, altern)]);
-            /*   fcx.ccx.tcx.sess.span_note(antec.span,
-               "poststate_res = " + aux::bitv_to_str(fcx, poststate_res));
+                intersect_states(block_poststate(fcx.ccx, conseq),
+                                    expr_poststate(fcx.ccx, altern));
+            /*
+               fcx.ccx.tcx.sess.span_note(antec.span,
+               "poststate_res = " + aux::tritv_to_str(fcx, poststate_res));
             fcx.ccx.tcx.sess.span_note(antec.span,
                "altern poststate = " +
-                aux::bitv_to_str(fcx, expr_poststate(fcx.ccx, altern)));
+                aux::tritv_to_str(fcx, expr_poststate(fcx.ccx, altern)));
             fcx.ccx.tcx.sess.span_note(antec.span,
-            "conseq poststate = " + aux::bitv_to_str(fcx,
-               block_poststate(fcx.ccx, conseq))); */
+            "conseq poststate = " + aux::tritv_to_str(fcx,
+               block_poststate(fcx.ccx, conseq))); 
+            */
 
             changed |= set_poststate_ann(fcx.ccx, id, poststate_res);
         }
@@ -287,7 +295,7 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
 }
 
 fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
-    auto num_local_vars = num_constraints(fcx.enclosing);
+    auto num_constrs = num_constraints(fcx.enclosing);
 
     alt (e.node) {
         case (expr_vec(?elts, _, _)) {
@@ -381,7 +389,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
                a ret expression (since execution never continues locally
                after a ret expression */
 
-            set_poststate_ann(fcx.ccx, e.id, false_postcond(num_local_vars));
+            set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs));
             /* return from an always-failing function clears the return bit */
 
             alt (fcx.enclosing.cf) {
@@ -401,7 +409,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
         }
         case (expr_be(?val)) {
             auto changed = set_prestate_ann(fcx.ccx, e.id, pres);
-            set_poststate_ann(fcx.ccx, e.id, false_postcond(num_local_vars));
+            set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs));
             ret changed | find_pre_post_state_expr(fcx, pres, val);
         }
         case (expr_if(?antec, ?conseq, ?maybe_alt)) {
@@ -423,55 +431,62 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
                                         oper_assign);
         }
         case (expr_while(?test, ?body)) {
-            auto changed = set_prestate_ann(fcx.ccx, e.id, pres) |
-            /* to handle general predicates, we need to pass in
-                pres `intersect` (poststate(a)) 
-             like: auto test_pres = intersect_postconds(pres,
-             expr_postcond(a)); However, this doesn't work right now because
-             we would be passing in an all-zero prestate initially
-               FIXME
-               maybe need a "don't know" state in addition to 0 or 1?
+            /*
+            log_err "in a while loop:";
+            log_expr_err(*e);
+            aux::log_tritv_err(fcx, block_poststate(fcx.ccx, body));
+            aux::log_tritv_err(fcx, pres);
             */
-                find_pre_post_state_expr(fcx, pres, test) |
+            auto loop_pres = intersect_states
+                (block_poststate(fcx.ccx, body), pres);
+            // aux::log_tritv_err(fcx, loop_pres);
+            // log_err "---------------";
+
+            auto changed = set_prestate_ann(fcx.ccx, e.id, loop_pres) |
+                find_pre_post_state_expr(fcx, loop_pres, test) |
                 find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, test),
                                           body);
             /* conservative approximation: if a loop contains a break
                or cont, we assume nothing about the poststate */
+            /* which is still unsound -- see [Break-unsound] */
             if (has_nonlocal_exits(body)) { 
-                changed |= set_poststate_ann(fcx.ccx, e.id, pres);
+                ret changed | set_poststate_ann(fcx.ccx, e.id, pres);
+            }
+            else {
+                auto e_post = expr_poststate(fcx.ccx, test);
+                auto b_post = block_poststate(fcx.ccx, body);
+                ret changed | set_poststate_ann
+                    (fcx.ccx, e.id, intersect_states(e_post, b_post));
             }
-
-            auto e_post = expr_poststate(fcx.ccx, test);
-            auto b_post = block_poststate(fcx.ccx, body);
-            ret changed | set_poststate_ann
-                (fcx.ccx, e.id, intersect_postconds([e_post, b_post]));
         }
         case (expr_do_while(?body, ?test)) {
-            auto changed = set_prestate_ann(fcx.ccx, e.id, pres);
-            auto changed0 = changed;
-            changed |= find_pre_post_state_block(fcx, pres, body);
+            auto loop_pres = intersect_states(expr_poststate(fcx.ccx, test),
+                                              pres);
+
+            auto changed = set_prestate_ann(fcx.ccx, e.id, loop_pres);
+            changed |= find_pre_post_state_block(fcx, loop_pres, body);
             /* conservative approximination: if the body of the loop
                could break or cont, we revert to the prestate
                (TODO: could treat cont differently from break, since
                if there's a cont, the test will execute) */
 
+            changed |= find_pre_post_state_expr
+                (fcx, block_poststate(fcx.ccx, body), test);
+
             auto breaks = has_nonlocal_exits(body);
             if (breaks) {
                 // this should probably be true_poststate and not pres,
                 // b/c the body could invalidate stuff
-                // FIXME
-                 // This doesn't set "changed", as if the previous state
-                // was different, this might come back true every time
-                set_poststate_ann(fcx.ccx, body.node.id, pres);
-                changed = changed0;
-            }
-
-            changed |= find_pre_post_state_expr
-                (fcx, block_poststate(fcx.ccx, body), test);
-
-            if (breaks) {
-                set_poststate_ann(fcx.ccx, e.id, pres);
-            }
+                // FIXME [Break-unsound]
+                // This is unsound as it is -- consider
+                // while (true) {
+                //    x <- y;
+                //    break;
+                // }
+                // The poststate wouldn't take into account that
+                // y gets deinitialized
+                changed |= set_poststate_ann(fcx.ccx, e.id, pres);
+             }
             else {
                 changed |= set_poststate_ann
                     (fcx.ccx, e.id, expr_poststate(fcx.ccx, test));
@@ -493,7 +508,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
             auto e_post = expr_poststate(fcx.ccx, val);
             auto a_post;
             if (vec::len[arm](alts) > 0u) {
-                a_post = false_postcond(num_local_vars);
+                a_post = false_postcond(num_constrs);
                 for (arm an_alt in alts) {
                     changed |= find_pre_post_state_block
                         (fcx, e_post, an_alt.block);
@@ -524,7 +539,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
             /* if execution continues after fail, then everything is true!
                woo! */
                 set_poststate_ann(fcx.ccx, e.id,
-                                  false_postcond(num_local_vars));
+                                  false_postcond(num_constrs));
         }
         case (expr_assert(?p)) {
             ret find_pre_post_state_sub(fcx, pres, p, e.id, none);
@@ -604,8 +619,12 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
                             */
                         }
                         case (none) {
-                            ret set_prestate(stmt_ann, pres) |
-                                set_poststate(stmt_ann, pres);
+                            // let int = x; => x is uninit in poststate
+                            set_poststate_ann(fcx.ccx, id, pres);
+                            clear_in_poststate_ident(fcx, alocal.node.id,
+                                                         alocal.node.ident, id);
+                            set_prestate(stmt_ann, pres);
+                            ret false;
                         }
                     }
                 }
@@ -683,6 +702,8 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
 
 fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool {
     auto num_local_vars = num_constraints(fcx.enclosing);
+    // make sure the return bit starts out False
+    clear_in_prestate_ident(fcx, fcx.id, fcx.name, f.body.node.id);
     auto changed =
         find_pre_post_state_block(fcx, block_prestate(fcx.ccx, f.body),
                                   f.body);
@@ -704,6 +725,13 @@ fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool {
         }
         case (none) {/* fallthrough */ }
     }
+
+/*
+    log_err "find_pre_post_state_fn";
+    log_err changed;
+    fcx.ccx.tcx.sess.span_note(f.body.span, fcx.name);
+*/
+
     ret changed;
 }
 //
diff --git a/src/comp/middle/tstate/tritv.rs b/src/comp/middle/tstate/tritv.rs
index 88bc74772b4..90be1810301 100644
--- a/src/comp/middle/tstate/tritv.rs
+++ b/src/comp/middle/tstate/tritv.rs
@@ -82,18 +82,32 @@ fn trit_or(trit a, trit b) -> trit {
   }
 }
 
+// FIXME: This still seems kind of dodgy to me (that is,
+// that 1 + ? = 1. But it might work out given that
+// all variables start out in a 0 state. Probably I need
+// to make it so that all constraints start out in a 0 state
+// (we consider a constraint false until proven true), too.
 fn trit_and(trit a, trit b) -> trit {
   alt (a) {
-    case (dont_care) { dont_care }
-    case (ttrue)     {
-      alt (b) {
-        case (dont_care) { dont_care }
-        case (ttrue)     { ttrue }
-        case (tfalse)    { dont_care } // ???
+      case (dont_care) { b }  // also seems wrong for case b = ttrue
+      case (ttrue)     {
+          alt (b) {
+              case (dont_care) { ttrue } // ??? Seems wrong
+              case (ttrue)     { ttrue }
+              // false wins, since if something is uninit
+              // on one path, we care
+              // (Rationale: it's always safe to assume that
+         // a var is uninitialized or that a constraint
+         // needs to be re-established)
+              case (tfalse)    { tfalse }
+          }
       }
-    }
+      // Rationale: if it's uninit on one path,
+      // we can consider it as uninit on all paths
     case (tfalse) { tfalse }
   }
+  // if the result is dont_care, that means
+  // a and b were both dont_care
 }
 
 fn change(bool changed, trit old, trit new) -> bool { changed || new != old }
diff --git a/src/test/compile-fail/do-while-constraints.rs b/src/test/compile-fail/do-while-constraints.rs
new file mode 100644
index 00000000000..c9c557320a0
--- /dev/null
+++ b/src/test/compile-fail/do-while-constraints.rs
@@ -0,0 +1,17 @@
+// xfail-stage0
+// error-pattern: Unsatisfied precondition constraint (for example, init(y
+fn main() {
+
+  let int y = 42;
+  let int x;
+  do {
+    log y;
+    do {
+      do {
+	do {
+	  x <- y;
+	} while (true);
+      } while (true);
+    } while (true);
+  } while (true);
+}
\ No newline at end of file
diff --git a/src/test/compile-fail/while-loop-constraints.rs b/src/test/compile-fail/while-loop-constraints.rs
new file mode 100644
index 00000000000..981a555ff30
--- /dev/null
+++ b/src/test/compile-fail/while-loop-constraints.rs
@@ -0,0 +1,17 @@
+// xfail-stage0
+// error-pattern: Unsatisfied precondition constraint (for example, init(y
+fn main() {
+
+  let int y = 42;
+  let int x;
+  while (true) {
+    log y;
+    while (true) {
+      while (true) {
+	while (true) {
+	  x <- y;
+	}
+      }
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/test/run-pass/while-loop-constraints-2.rs b/src/test/run-pass/while-loop-constraints-2.rs
new file mode 100644
index 00000000000..c1550ad2d08
--- /dev/null
+++ b/src/test/run-pass/while-loop-constraints-2.rs
@@ -0,0 +1,16 @@
+// xfail-stage0
+fn main() {
+
+  let int y = 42;
+  let int z = 42;
+  let int x;
+  while (z < 50) {
+    z += 1; 
+    while (false) {
+      x <- y;
+      y = z;
+    }
+    log y;
+  }
+  assert (y == 42 && z == 50);
+}
\ No newline at end of file