diff --git a/src/comp/middle/tstate/ann.rs b/src/comp/middle/tstate/ann.rs
index a1b5508e2a2d..a894dde11a64 100644
--- a/src/comp/middle/tstate/ann.rs
+++ b/src/comp/middle/tstate/ann.rs
@@ -1,36 +1,36 @@
 
 import front::ast::ident;
 import std::vec;
-import std::bitv;
+import tritv::*;
 
+type precond = t;
+
+/* 2 means "this constraint may or may not be true after execution" 
+   1 means "this constraint is definitely true after execution"
+   0 means "this constraint is definitely false after execution" */
+type postcond = t;
+
+
+/* 2 means "don't know about this constraint"
+   1 means "this constraint is definitely true before entry"
+   0 means "this constraint is definitely false on entry" */
+type prestate = t;
+
+
+/* similar to postcond */
+type poststate = t;
+
+
+/* 1 means "this variable is definitely initialized"
+  0 means "don't know whether this variable is
+  initialized" */
 
 /* 
-   This says: this expression requires the idents in <pre> to be initialized,
-   and given the precondition, it guarantees that the idents in <post> are
-   initialized.
+   This says: this expression requires the constraints whose value is 1 in
+   <pre> to be true, and given the precondition, it guarantees that the
+   constraints in <post> whose values are 1 are true, and that the constraints
+   in <post> whose values are 0 are false.
  */
-type precond = bitv::t;
-
-
-/* 1 means "this variable must be initialized"
-  0 means "don't care about this variable" */
-type postcond = bitv::t;
-
-
-/* 1 means "this variable is initialized"
-  0 means "don't know about this variable */
-type prestate = bitv::t;
-
-
-/* 1 means "this variable is definitely initialized"
-  0 means "don't know whether this variable is
-  initialized" */
-type poststate = bitv::t;
-
-
-/* 1 means "this variable is definitely initialized"
-  0 means "don't know whether this variable is
-  initialized" */
 
 /* named thus so as not to confuse with prestate and poststate */
 type pre_and_post = @rec(precond precondition, postcond postcondition);
@@ -44,7 +44,7 @@ type pre_and_post_state = rec(prestate prestate, poststate poststate);
 type ts_ann = @rec(pre_and_post conditions, pre_and_post_state states);
 
 fn true_precond(uint num_vars) -> precond {
-    be bitv::create(num_vars, false);
+    be create_tritv(num_vars);
 }
 
 fn true_postcond(uint num_vars) -> postcond { be true_precond(num_vars); }
@@ -54,7 +54,9 @@ fn empty_prestate(uint num_vars) -> prestate { be true_precond(num_vars); }
 fn empty_poststate(uint num_vars) -> poststate { be true_precond(num_vars); }
 
 fn false_postcond(uint num_vars) -> postcond {
-    be bitv::create(num_vars, true);
+    auto res = create_tritv(num_vars);
+    tritv_set_all(res);
+    ret res;
 }
 
 fn empty_pre_post(uint num_vars) -> pre_and_post {
@@ -77,12 +79,16 @@ fn get_pre(&pre_and_post p) -> precond { ret p.precondition; }
 fn get_post(&pre_and_post p) -> postcond { ret p.postcondition; }
 
 fn difference(&precond p1, &precond p2) -> bool {
-    be bitv::difference(p1, p2);
+    ret tritv_difference(p1, p2);
 }
 
-fn union(&precond p1, &precond p2) -> bool { be bitv::union(p1, p2); }
+fn union(&precond p1, &precond p2) -> bool {
+    ret tritv_union(p1, p2);
+}
 
-fn intersect(&precond p1, &precond p2) -> bool { be bitv::intersect(p1, p2); }
+fn intersect(&precond p1, &precond p2) -> bool {
+    ret tritv_intersect(p1, p2);
+}
 
 fn pps_len(&pre_and_post p) -> uint {
     // gratuitous check
@@ -93,86 +99,88 @@ fn pps_len(&pre_and_post p) -> uint {
 
 fn require(uint i, &pre_and_post p) {
     // sets the ith bit in p's pre
-
-    bitv::set(p.precondition, i, true);
+    tritv_set(i, p.precondition, ttrue);
 }
 
 fn require_and_preserve(uint i, &pre_and_post p) {
     // sets the ith bit in p's pre and post
-
-    bitv::set(p.precondition, i, true);
-    bitv::set(p.postcondition, i, true);
+    tritv_set(i, p.precondition, ttrue);
+    tritv_set(i, p.postcondition, ttrue);
 }
 
 fn set_in_postcond(uint i, &pre_and_post p) -> bool {
     // sets the ith bit in p's post
-
-    auto was_set = bitv::get(p.postcondition, i);
-    bitv::set(p.postcondition, i, true);
-    ret !was_set;
+    auto was_set = tritv_get(p.postcondition, i);
+    tritv_set(i, p.postcondition, ttrue);
+    ret was_set != ttrue;
 }
 
 fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
     // sets the ith bit in p's post
-
-    auto was_set = bitv::get(s.poststate, i);
-    bitv::set(s.poststate, i, true);
-    ret !was_set;
+    auto was_set = tritv_get(s.poststate, i);
+    tritv_set(i, s.poststate, ttrue);
+    ret was_set != ttrue;
 }
 
 fn clear_in_poststate(uint i, &pre_and_post_state s) -> bool {
     // sets the ith bit in p's post
-
-    auto was_set = bitv::get(s.poststate, i);
-    bitv::set(s.poststate, i, false);
-    ret was_set;
+    auto was_set = tritv_get(s.poststate, i);
+    tritv_set(i, s.poststate, 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 != tfalse;
+}
 
 // Sets all the bits in a's precondition to equal the
 // corresponding bit in p's precondition.
 fn set_precondition(ts_ann a, &precond p) {
-    bitv::copy(a.conditions.precondition, p);
+    tritv_copy(a.conditions.precondition, p);
 }
 
 
 // Sets all the bits in a's postcondition to equal the
 // corresponding bit in p's postcondition.
 fn set_postcondition(ts_ann a, &postcond p) {
-    bitv::copy(a.conditions.postcondition, p);
+    tritv_copy(a.conditions.postcondition, p);
 }
 
 
 // Sets all the bits in a's prestate to equal the
 // corresponding bit in p's prestate.
 fn set_prestate(ts_ann a, &prestate p) -> bool {
-    ret bitv::copy(a.states.prestate, p);
+    ret tritv_copy(a.states.prestate, p);
 }
 
 
 // Sets all the bits in a's postcondition to equal the
 // corresponding bit in p's postcondition.
 fn set_poststate(ts_ann a, &poststate p) -> bool {
-    ret bitv::copy(a.states.poststate, p);
+    ret tritv_copy(a.states.poststate, p);
 }
 
 
 // Set all the bits in p that are set in new
 fn extend_prestate(&prestate p, &poststate new) -> bool {
-    ret bitv::union(p, new);
+    ret tritv_union(p, new);
 }
 
 
 // Set all the bits in p that are set in new
 fn extend_poststate(&poststate p, &poststate new) -> bool {
-    ret bitv::union(p, new);
+    ret tritv_union(p, new);
 }
 
-// Clears the given bit in p
+// Sets the given bit in p to "don't care"
+// FIXME: is this correct?
 fn relax_prestate(uint i, &prestate p) -> bool {
-    auto was_set = bitv::get(p, i);
-    bitv::set(p, i, false);
-    ret was_set;
+    auto was_set = tritv_get(p, i);
+    tritv_set(i, p, dont_care);
+    ret was_set != dont_care;
 }
 
 // Clears the given bit in p
@@ -185,12 +193,11 @@ fn relax_precond(uint i, &precond p) {
     relax_prestate(i, p);
 }
 
-// Clears all the bits in p
-fn clear(&precond p) { bitv::clear(p); }
+// Sets all the bits in p to "don't care"
+fn clear(&precond p) { tritv_clear(p); }
 
-
-// Sets all the bits in p
-fn set(&precond p) { bitv::set_all(p); }
+// Sets all the bits in p to true
+fn set(&precond p) { tritv_set_all(p); }
 
 fn ann_precond(&ts_ann a) -> precond { ret a.conditions.precondition; }
 
@@ -203,16 +210,17 @@ fn pp_clone(&pre_and_post p) -> pre_and_post {
              postcondition=clone(p.postcondition));
 }
 
-fn clone(prestate p) -> prestate { ret bitv::clone(p); }
+fn clone(prestate p) -> prestate { ret tritv_clone(p); }
 
 
 // returns true if a implies b
 // that is, returns true except if for some bits c and d,
-// c = 1 and d = 0
-fn implies(bitv::t a, bitv::t b) -> bool {
-    auto tmp = bitv::clone(b);
-    bitv::difference(tmp, a);
-    ret bitv::is_false(tmp);
+// c = 1 and d = either 0 or "don't know"
+// FIXME: is this correct?
+fn implies(t a, t b) -> bool {
+    auto tmp = tritv_clone(b);
+    tritv_difference(tmp, a);
+    ret tritv_doesntcare(tmp);
 }
 //
 // Local Variables:
diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs
index d2f068ba5dc6..a21db0407b28 100644
--- a/src/comp/middle/tstate/auxiliary.rs
+++ b/src/comp/middle/tstate/auxiliary.rs
@@ -1,5 +1,3 @@
-
-import std::bitv;
 import std::str;
 import std::vec;
 import std::vec::len;
@@ -39,6 +37,10 @@ import tstate::ann::extend_poststate;
 import tstate::ann::set_precondition;
 import tstate::ann::set_postcondition;
 import tstate::ann::ts_ann;
+import tstate::ann::clear_in_postcond;
+import tstate::ann::clear_in_poststate;
+import tritv::*;
+
 import pretty::ppaux::constr_args_to_str;
 import pretty::ppaux::lit_to_str;
 
@@ -53,7 +55,7 @@ fn comma_str(vec[@constr_arg_use] args) -> str {
         if (comma) { res += ", "; } else { comma = true; }
         alt (a.node) {
             case (carg_base) { res += "*"; }
-            case (carg_ident(?i)) { res += i; }
+            case (carg_ident(?i)) { res += i._0; }
             case (carg_lit(?l)) { res += lit_to_str(l); }
         }
     }
@@ -72,29 +74,33 @@ fn constraint_to_str(&ty::ctxt tcx, &constr c) -> str {
     }
 }
 
-fn bitv_to_str(fn_ctxt fcx, bitv::t v) -> str {
+fn tritv_to_str(fn_ctxt fcx, &tritv::t v) -> str {
     auto s = "";
     auto comma = false;
     for (norm_constraint p in constraints(fcx)) {
-        if (bitv::get(v, p.bit_num)) {
-            s +=
-                if (comma) { ", " } else { comma = true; "" } +
-                    aux::constraint_to_str(fcx.ccx.tcx, p.c);
+        alt (tritv_get(v, p.bit_num)) {
+            case (dont_care) { }
+            case (?t) {
+                s +=
+                    if (comma) { ", " } else { comma = true; "" } +
+                    if (t == tfalse) { "!" } else { "" } +                  
+                    constraint_to_str(fcx.ccx.tcx, p.c);
+            }
         }
     }
     ret s;
 }
 
-fn log_bitv(&fn_ctxt fcx, &bitv::t v) { log bitv_to_str(fcx, v); }
+fn log_tritv(&fn_ctxt fcx, &tritv::t v) { log tritv_to_str(fcx, v); }
 
-fn first_difference_string(&fn_ctxt fcx, &bitv::t expected, &bitv::t actual)
+fn first_difference_string(&fn_ctxt fcx, &tritv::t expected, &tritv::t actual)
    -> str {
     let str s = "";
     auto done = false;
     for (norm_constraint c in constraints(fcx)) {
         if (!done) {
-            if (bitv::get(expected, c.bit_num) &&
-                    !bitv::get(actual, c.bit_num)) {
+            if (tritv_get(expected, c.bit_num) == ttrue &&
+                tritv_get(actual, c.bit_num) != ttrue) {
                 /*
                   FIXME
                   for fun, try either:
@@ -111,11 +117,13 @@ fn first_difference_string(&fn_ctxt fcx, &bitv::t expected, &bitv::t actual)
     ret s;
 }
 
-fn log_bitv_err(fn_ctxt fcx, bitv::t v) { log_err bitv_to_str(fcx, v); }
+fn log_tritv_err(fn_ctxt fcx, tritv::t v) { log_err tritv_to_str(fcx, v); }
 
 fn tos(vec[uint] v) -> str {
     auto res = "";
-    for (uint i in v) { if (i == 0u) { res += "0"; } else { res += "1"; } }
+    for (uint i in v) { if (i == 0u) { res += "0"; } 
+        else if (i == 1u) { res += "1"; }
+        else { res += "?"; } }
     ret res;
 }
 
@@ -124,8 +132,8 @@ fn log_cond(vec[uint] v) { log tos(v); }
 fn log_cond_err(vec[uint] v) { log_err tos(v); }
 
 fn log_pp(&pre_and_post pp) {
-    auto p1 = bitv::to_vec(pp.precondition);
-    auto p2 = bitv::to_vec(pp.postcondition);
+    auto p1 = tritv::to_vec(pp.precondition);
+    auto p2 = tritv::to_vec(pp.postcondition);
     log "pre:";
     log_cond(p1);
     log "post:";
@@ -133,8 +141,8 @@ fn log_pp(&pre_and_post pp) {
 }
 
 fn log_pp_err(&pre_and_post pp) {
-    auto p1 = bitv::to_vec(pp.precondition);
-    auto p2 = bitv::to_vec(pp.postcondition);
+    auto p1 = tritv::to_vec(pp.precondition);
+    auto p2 = tritv::to_vec(pp.postcondition);
     log_err "pre:";
     log_cond_err(p1);
     log_err "post:";
@@ -142,8 +150,8 @@ fn log_pp_err(&pre_and_post pp) {
 }
 
 fn log_states(&pre_and_post_state pp) {
-    auto p1 = bitv::to_vec(pp.prestate);
-    auto p2 = bitv::to_vec(pp.poststate);
+    auto p1 = tritv::to_vec(pp.prestate);
+    auto p2 = tritv::to_vec(pp.poststate);
     log "prestate:";
     log_cond(p1);
     log "poststate:";
@@ -151,8 +159,8 @@ fn log_states(&pre_and_post_state pp) {
 }
 
 fn log_states_err(&pre_and_post_state pp) {
-    auto p1 = bitv::to_vec(pp.prestate);
-    auto p2 = bitv::to_vec(pp.poststate);
+    auto p1 = tritv::to_vec(pp.prestate);
+    auto p2 = tritv::to_vec(pp.poststate);
     log_err "prestate:";
     log_cond_err(p1);
     log_err "poststate:";
@@ -202,7 +210,7 @@ type pred_desc_ = rec(vec[@constr_arg_use] args, uint bit_num);
 
 type pred_desc = spanned[pred_desc_];
 
-type constr_arg_use = constr_arg_general[ident];
+type constr_arg_use = constr_arg_general[tup(ident, def_id)];
 
 tag constraint {
     cinit(uint, span, ident);
@@ -377,12 +385,6 @@ fn block_poststate(&crate_ctxt ccx, &block b) -> poststate {
     ret block_states(ccx, b).poststate;
 }
 
-
-/* sets the pre_and_post for an ann */
-fn with_pp(&crate_ctxt ccx, node_id id, pre_and_post p) {
-    add_node(ccx, id, @rec(conditions=p, states=empty_states(pps_len(p))));
-}
-
 fn set_prestate_ann(&crate_ctxt ccx, node_id id, &prestate pre) -> bool {
     log "set_prestate_ann";
     ret set_prestate(node_id_to_ts_ann(ccx, id), pre);
@@ -519,17 +521,16 @@ fn constraints(&fn_ctxt fcx) -> vec[norm_constraint] {
     ret res;
 }
 
-
-// FIXME:
-// this probably doesn't handle name shadowing well (or at all)
-// variables should really always be id'd by def_id and not ident
 fn match_args(&fn_ctxt fcx, vec[pred_desc] occs, vec[@constr_arg_use] occ) ->
    uint {
     log "match_args: looking at " +
-            pretty::ppaux::constr_args_to_str(std::util::id[str], occ);
+        pretty::ppaux::constr_args_to_str(std::util::fst[ident, def_id], occ);
     for (pred_desc pd in occs) {
         log "match_args: candidate " + pred_desc_to_str(pd);
-        if (ty::args_eq(str::eq, pd.node.args, occ)) { ret pd.node.bit_num; }
+        fn eq(&tup(ident, def_id) p, &tup(ident, def_id) q) -> bool {
+            ret p._1 == q._1;
+        }
+        if (ty::args_eq(eq, pd.node.args, occ)) { ret pd.node.bit_num; }
     }
     fcx.ccx.tcx.sess.bug("match_args: no match for occurring args");
 }
@@ -549,11 +550,20 @@ fn node_id_for_constr(ty::ctxt tcx, node_id t) -> node_id {
 fn expr_to_constr_arg(ty::ctxt tcx, &@expr e) -> @constr_arg_use {
     alt (e.node) {
         case (expr_path(?p)) {
-            if (vec::len(p.node.idents) == 1u) {
-                ret @respan(p.span, carg_ident[ident](p.node.idents.(0)));
-            } else {
-                tcx.sess.bug("exprs_to_constr_args: non-local variable " +
+            alt (tcx.def_map.find(e.id)) {
+                case (some(def_local(?l_id))) {
+                    ret @respan(p.span, carg_ident(tup(p.node.idents.(0),
+                                                       l_id)));
+                }
+                case (some(def_arg(?a_id))) {
+                    ret @respan(p.span, carg_ident(tup(p.node.idents.(0),
+                                                       a_id)));
+                }
+                case (_) {
+                    tcx.sess.bug("exprs_to_constr_args: non-local variable " +
                                  "as pred arg");
+                        
+                }
             }
         }
         case (expr_lit(?l)) { ret @respan(e.span, carg_lit(l)); }
@@ -601,8 +611,8 @@ fn expr_to_constr(ty::ctxt tcx, &@expr e) -> constr {
 
 fn pred_desc_to_str(&pred_desc p) -> str {
     ret "<" + uistr(p.node.bit_num) + ", " +
-            pretty::ppaux::constr_args_to_str(std::util::id[str], p.node.args)
-            + ">";
+        pretty::ppaux::constr_args_to_str(std::util::fst[ident, def_id],
+                                          p.node.args) + ">";
 }
 
 fn substitute_constr_args(&ty::ctxt cx, &vec[@expr] actuals,
@@ -644,6 +654,77 @@ tag if_ty {
     if_check;
     plain_if;
 }
+
+fn local_node_id_to_def_id(&fn_ctxt fcx, &span sp, &node_id i) -> def_id {
+    alt (fcx.ccx.tcx.def_map.find(i)) {
+        case (some(def_local(?d_id))) {
+            ret d_id;
+        }
+        case (some (def_arg(?a_id))) {
+            ret a_id;
+        }
+        case (some(_)) {
+            fcx.ccx.tcx.sess.span_fatal(sp, "local_node_id_to_def_id: id \
+               isn't a local");
+        }
+        case (none) {
+            // should really be bug. span_bug()?
+            fcx.ccx.tcx.sess.span_fatal(sp, "local_node_id_to_def_id: id \
+               is unbound");
+        }
+    }
+}
+
+fn forget_in_postcond(&fn_ctxt fcx, &span dead_sp,
+                      node_id parent_exp, node_id dead_v) {
+    // In the postcondition given by parent_exp, clear the bits
+    // for any constraints mentioning dead_v
+    auto d_id = local_node_id_to_def_id(fcx, dead_sp, dead_v);
+    for (norm_constraint c in constraints(fcx)) {
+        if (constraint_mentions(fcx, c, d_id)) {
+            clear_in_postcond(c.bit_num,
+              node_id_to_ts_ann(fcx.ccx, parent_exp).conditions);
+        }
+    }
+}
+
+fn forget_in_poststate(&fn_ctxt fcx, &span dead_sp, 
+                       node_id parent_exp, node_id dead_v) -> bool {
+    // In the poststate given by parent_exp, clear the bits
+    // for any constraints mentioning dead_v
+    auto d_id = local_node_id_to_def_id(fcx, dead_sp, dead_v);
+    auto changed = false;
+    for (norm_constraint c in constraints(fcx)) {
+        if (constraint_mentions(fcx, c, d_id)) {
+            changed = clear_in_poststate(c.bit_num,
+              node_id_to_ts_ann(fcx.ccx, parent_exp).states) || changed;
+        }
+    }
+    ret changed;
+}
+
+fn constraint_mentions(&fn_ctxt fcx, &norm_constraint c, &def_id v) -> bool {
+    ret (alt (c.c.node.c) {
+            case (ninit(_)) {
+                v == local_def(c.c.node.id)
+            }
+            case (npred(_, ?args)) {
+                args_mention(args, v)
+            }
+        });
+}
+
+
+fn args_mention(&vec[@constr_arg_use] args, &def_id v) -> bool {
+    fn mentions(&def_id v, &@constr_arg_use a) -> bool {
+        alt (a.node) {
+            case (carg_ident(?p1)) { p1._1 == v }
+            case (_)               { false }
+        }
+    }
+    ret util::common::any[@constr_arg_use](bind mentions(v,_), args);
+}
+
 //
 // Local Variables:
 // mode: rust
diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs
index 3850986a4f8f..d29e57c7d301 100644
--- a/src/comp/middle/tstate/bitvectors.rs
+++ b/src/comp/middle/tstate/bitvectors.rs
@@ -1,12 +1,11 @@
-
-import std::bitv;
+import front::ast::*;
 import std::vec;
 import std::vec::len;
 import std::vec::slice;
-import front::ast::*;
 import aux::fn_ctxt;
 import aux::fn_info;
-import aux::log_bitv;
+import aux::log_tritv;
+import aux::log_tritv_err;
 import aux::num_constraints;
 import aux::cinit;
 import aux::cpred;
@@ -40,6 +39,7 @@ import tstate::ann::clone;
 import tstate::ann::set_in_postcond;
 import tstate::ann::set_in_poststate;
 import tstate::ann::clear_in_poststate;
+import tritv::*;
 
 fn bit_num(&fn_ctxt fcx, &constr_ c) -> uint {
     assert (fcx.enclosing.constrs.contains_key(c.id));
@@ -67,57 +67,81 @@ fn bit_num(&fn_ctxt fcx, &constr_ c) -> uint {
 }
 
 fn promises(&fn_ctxt fcx, &poststate p, &constr_ c) -> bool {
-    ret bitv::get(p, bit_num(fcx, c));
+    ret tritv_get(p, bit_num(fcx, c)) == ttrue;
 }
 
+// v "happens after" u
+fn seq_trit(trit u, trit v) -> trit {
+    alt (v) {
+        case (ttrue)     { ttrue }
+        case (tfalse)    { tfalse }
+        case (dont_care) { u }
+    }
+}
+
+// idea: q "happens after" p -- so if something is
+// 1 in q and 0 in p, it's 1 in the result; however,
+// if it's 0 in q and 1 in p, it's 0 in the result
+fn seq_tritv(&postcond p, &postcond q) {
+    auto i = 0u;
+    assert (p.nbits == q.nbits);
+    while (i < p.nbits) {
+        tritv_set(i, p, seq_trit(tritv_get(p, i), tritv_get(q, i)));
+        i += 1u;
+    }
+}
+
+fn seq_postconds(&fn_ctxt fcx, &vec[postcond] ps) -> postcond {
+    auto sz = vec::len(ps);
+    if (sz >= 1u) {
+        auto prev = tritv_clone(ps.(0));
+        for (postcond p in slice(ps, 1u, sz)) {
+            seq_tritv(prev, p);
+        }
+        ret prev;
+    }
+    else {
+        ret ann::empty_poststate(num_constraints(fcx.enclosing));
+    }
+}
 
 // Given a list of pres and posts for exprs e0 ... en,
 // 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_ctxt fcx, vec[pre_and_post] pps) -> precond {
-    let uint sz = len[pre_and_post](pps);
+fn seq_preconds(&fn_ctxt fcx, &vec[pre_and_post] pps) -> precond {
+    let uint sz = len(pps);
     let uint num_vars = num_constraints(fcx.enclosing);
+
+    fn seq_preconds_go(&fn_ctxt fcx, &vec[pre_and_post] pps,
+                       &pre_and_post first)
+        -> precond {
+        let uint sz = len(pps);
+        if (sz >= 1u) {
+            auto second = pps.(0);
+            assert (pps_len(second) == num_constraints(fcx.enclosing));
+            auto second_pre = clone(second.precondition);
+            difference(second_pre, first.postcondition);
+            auto next_first = clone(first.precondition);
+            union(next_first, second_pre);
+            auto next_first_post = clone(first.postcondition);
+            seq_tritv(next_first_post, second.postcondition); 
+            ret seq_preconds_go(fcx, slice(pps, 1u, sz), 
+                                @rec(precondition=next_first,
+                                     postcondition=next_first_post));
+        }
+        else {
+            ret first.precondition;
+        }
+    }
+
     if (sz >= 1u) {
         auto first = pps.(0);
         assert (pps_len(first) == num_vars);
-        let precond rest =
-            seq_preconds(fcx, slice[pre_and_post](pps, 1u, sz));
-        difference(rest, first.postcondition);
-        auto res = clone(first.precondition);
-        union(res, rest);
-        log "seq_preconds:";
-        log "first.postcondition =";
-        log_bitv(fcx, first.postcondition);
-        log "rest =";
-        log_bitv(fcx, rest);
-        log "returning";
-        log_bitv(fcx, res);
-        ret res;
+        ret seq_preconds_go(fcx, slice(pps, 1u, sz), first);
     } else { ret true_precond(num_vars); }
 }
 
-
-/* works on either postconds or preconds
- should probably rethink the whole type synonym situation */
-fn union_postconds_go(&postcond first, &vec[postcond] rest) -> postcond {
-    auto sz = vec::len[postcond](rest);
-    if (sz > 0u) {
-        auto other = rest.(0);
-        union(first, other);
-        union_postconds_go(first,
-                           slice[postcond](rest, 1u, len[postcond](rest)));
-    }
-    ret first;
-}
-
-fn union_postconds(uint nv, &vec[postcond] pcs) -> postcond {
-    if (len[postcond](pcs) > 0u) {
-        ret union_postconds_go(bitv::clone(pcs.(0)), pcs);
-    } else { ret empty_prestate(nv); }
-}
-
-
 /* Gee, maybe we could use foldl or something */
 fn intersect_postconds_go(&postcond first, &vec[postcond] rest) -> postcond {
     auto sz = vec::len[postcond](rest);
@@ -133,7 +157,7 @@ fn intersect_postconds_go(&postcond first, &vec[postcond] rest) -> postcond {
 
 fn intersect_postconds(&vec[postcond] pcs) -> postcond {
     assert (len[postcond](pcs) > 0u);
-    ret intersect_postconds_go(bitv::clone(pcs.(0)), pcs);
+    ret intersect_postconds_go(tritv_clone(pcs.(0)), pcs);
 }
 
 fn gen(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
diff --git a/src/comp/middle/tstate/ck.rs b/src/comp/middle/tstate/ck.rs
index 27933ee8eab1..444880e02cac 100644
--- a/src/comp/middle/tstate/ck.rs
+++ b/src/comp/middle/tstate/ck.rs
@@ -51,11 +51,11 @@ import aux::stmt_poststate;
 import aux::stmt_to_ann;
 import aux::num_constraints;
 import aux::fixed_point_states;
-import aux::bitv_to_str;
+import aux::tritv_to_str;
 import aux::first_difference_string;
 import pretty::pprust::ty_to_str;
 import util::common::log_stmt_err;
-import aux::log_bitv_err;
+import aux::log_tritv_err;
 import bitvectors::promises;
 import annotate::annotate_crate;
 import collect_locals::mk_f_to_fn_info;
@@ -83,9 +83,9 @@ fn check_states_expr(&fn_ctxt fcx, &@expr e) {
                 ") for expression:\n";
         s += pretty::pprust::expr_to_str(e);
         s += "\nPrecondition:\n";
-        s += bitv_to_str(fcx, prec);
+        s += tritv_to_str(fcx, prec);
         s += "\nPrestate:\n";
-        s += bitv_to_str(fcx, pres);
+        s += tritv_to_str(fcx, pres);
         fcx.ccx.tcx.sess.span_fatal(e.span, s);
     }
 }
@@ -112,9 +112,9 @@ fn check_states_stmt(&fn_ctxt fcx, &@stmt s) {
                 ") for statement:\n";
         ss += pretty::pprust::stmt_to_str(*s);
         ss += "\nPrecondition:\n";
-        ss += bitv_to_str(fcx, prec);
+        ss += tritv_to_str(fcx, prec);
         ss += "\nPrestate: \n";
-        ss += bitv_to_str(fcx, pres);
+        ss += tritv_to_str(fcx, pres);
         fcx.ccx.tcx.sess.span_fatal(s.span, ss);
     }
 }
diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs
index 8c7cb5067a7c..91d1f82f366d 100644
--- a/src/comp/middle/tstate/pre_post_conditions.rs
+++ b/src/comp/middle/tstate/pre_post_conditions.rs
@@ -47,18 +47,23 @@ import aux::expr_to_constr;
 import aux::if_ty;
 import aux::if_check;
 import aux::plain_if;
+import aux::forget_in_postcond;
 
 import aux::constraints_expr;
 import aux::substitute_constr_args;
 import aux::ninit;
 import aux::npred;
 import aux::path_to_ident;
-import bitvectors::seq_preconds;
-import bitvectors::union_postconds;
-import bitvectors::intersect_postconds;
 import bitvectors::bit_num;
-import bitvectors::gen;
+import bitvectors::promises;
+import bitvectors::seq_preconds;
+import bitvectors::seq_postconds;
+import bitvectors::intersect_postconds;
+import bitvectors::declare_var;
+import bitvectors::gen_poststate;
+import bitvectors::kill_poststate;
 import bitvectors::relax_precond_block;
+import bitvectors::gen;
 import front::ast::*;
 import util::common::new_int_hash;
 import util::common::new_def_hash;
@@ -153,9 +158,7 @@ fn find_pre_post_exprs(&fn_ctxt fcx, &vec[@expr] args, node_id id) {
     auto pps = vec::map[@expr, pre_and_post](g, args);
     auto h = get_post;
     set_pre_and_post(fcx.ccx, id, seq_preconds(fcx, pps),
-                     union_postconds(nv,
-                                     vec::map[pre_and_post,
-                                              postcond](h, pps)));
+                     seq_postconds(fcx, vec::map(h, pps)));
 }
 
 fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, &block body,
@@ -212,9 +215,8 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
                              [expr_pp(fcx.ccx, antec),
                               expr_pp(fcx.ccx, altern)]);
             auto postcond_false_case =
-                union_postconds(num_local_vars,
-                                [expr_postcond(fcx.ccx, antec),
-                                 expr_postcond(fcx.ccx, altern)]);
+                seq_postconds(fcx, [expr_postcond(fcx.ccx, antec),
+                                    expr_postcond(fcx.ccx, altern)]);
 
             /* Be sure to set the bit for the check condition here,
              so that it's *not* set in the alternative. */
@@ -230,14 +232,12 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
                              [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)]);
+                seq_postconds(fcx, [expr_postcond(fcx.ccx, antec),
+                                    block_postcond(fcx.ccx, conseq)]);
 
             auto precond_res =
-                union_postconds(num_local_vars,
-                                [precond_true_case,
-                                 precond_false_case]);
+                seq_postconds(fcx, [precond_true_case,
+                                    precond_false_case]);
             auto postcond_res =
                 intersect_postconds([postcond_true_case,
                                      postcond_false_case]);
@@ -274,7 +274,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
     auto num_local_vars = num_constraints(enclosing);
     fn do_rand_(fn_ctxt fcx, &@expr e) { find_pre_post_expr(fcx, e); }
     log "find_pre_post_expr (num_constraints =" + uistr(num_local_vars) +
-            "):";
+        "):";
     log_expr(*e);
     alt (e.node) {
         case (expr_call(?operator, ?operands)) {
@@ -288,13 +288,13 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
             auto pp = expr_pp(fcx.ccx, e);
             for (@ty::constr_def c in constraints_expr(fcx.ccx.tcx, operator))
                 {
-                auto i =
-                    bit_num(fcx,
-                            rec(id=c.node.id._1,
-                                c=substitute_constr_args(fcx.ccx.tcx,
-                                                         operands, c)));
-                require(i, pp);
-            }
+                    auto i =
+                        bit_num(fcx,
+                                rec(id=c.node.id._1,
+                                    c=substitute_constr_args(fcx.ccx.tcx,
+                                                             operands, c)));
+                    require(i, pp);
+                }
 
             /* if this is a failing call, its postcondition sets everything */
             alt (controlflow_expr(fcx.ccx, operator)) {
@@ -359,17 +359,17 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
             find_pre_post_exprs(fcx, es, e.id);
         }
         case (expr_move(?lhs, ?rhs)) {
-            // FIXME: this needs to deinitialize the rhs
             alt (lhs.node) {
                 case (expr_path(?p)) {
                     gen_if_local(fcx, lhs, rhs, e.id, lhs.id, p);
                 }
                 case (_) { find_pre_post_exprs(fcx, [lhs, rhs], e.id); }
             }
+            forget_in_postcond(fcx, rhs.span, e.id, rhs.id);
         }
         case (expr_swap(?lhs, ?rhs)) {
             // Both sides must already be initialized
-
+            
             find_pre_post_exprs(fcx, [lhs, rhs], e.id);
         }
         case (expr_assign(?lhs, ?rhs)) {
@@ -455,9 +455,8 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
             find_pre_post_block(fcx, body);
             find_pre_post_expr(fcx, test);
             auto loop_postcond =
-                union_postconds(num_local_vars,
-                                [block_postcond(fcx.ccx, body),
-                                 expr_postcond(fcx.ccx, test)]);
+                seq_postconds(fcx, [block_postcond(fcx.ccx, body),
+                                    expr_postcond(fcx.ccx, test)]);
             /* conservative approximination: if the body
                could break or cont, the test may never be executed */
 
@@ -566,6 +565,9 @@ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s) {
                 case (decl_local(?alocal)) {
                     alt (alocal.node.init) {
                         case (some(?an_init)) {
+                            /* LHS always becomes initialized,
+                             whether or not this is a move */
+
                             find_pre_post_expr(fcx, an_init.expr);
                             copy_pre_post(fcx.ccx, alocal.node.id, 
                                           an_init.expr);
@@ -576,6 +578,15 @@ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s) {
                             gen(fcx, id,
                                 rec(id=alocal.node.id, 
                                     c=ninit(alocal.node.ident)));
+                            
+                            alt (an_init.op) {
+                                case (init_move) {
+                                    forget_in_postcond(fcx, an_init.expr.span,
+                                                       id, an_init.expr.id);
+                                }
+                                case (_) { /* nothing gets deinitialized */ } 
+                            }
+
                         }
                         case (none) {
                             clear_pp(node_id_to_ts_ann(fcx.ccx,
@@ -643,6 +654,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, pps);
     auto h = get_post;
     auto postconds = vec::map[pre_and_post, postcond](h, pps);
@@ -654,7 +666,7 @@ fn find_pre_post_block(&fn_ctxt fcx, block b) {
     /* conservative approximation */
 
     if (!has_nonlocal_exits(b)) {
-        block_postcond = union_postconds(nv, postconds);
+        block_postcond = seq_postconds(fcx, postconds);
     }
     set_pre_and_post(fcx.ccx, b.node.id, block_precond, block_postcond);
 }
diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs
index 2efcb672794e..1637924d0a59 100644
--- a/src/comp/middle/tstate/states.rs
+++ b/src/comp/middle/tstate/states.rs
@@ -1,5 +1,3 @@
-
-import std::bitv;
 import std::vec;
 import std::vec::plus_option;
 import std::vec::cat_options;
@@ -15,7 +13,6 @@ import tstate::ann::postcond;
 import tstate::ann::empty_pre_post;
 import tstate::ann::empty_poststate;
 import tstate::ann::require_and_preserve;
-import tstate::ann::union;
 import tstate::ann::intersect;
 import tstate::ann::empty_prestate;
 import tstate::ann::prestate;
@@ -48,8 +45,8 @@ import aux::extend_poststate_ann;
 import aux::set_prestate_ann;
 import aux::set_poststate_ann;
 import aux::pure_exp;
-import aux::log_bitv;
-import aux::log_bitv_err;
+import aux::log_tritv;
+import aux::log_tritv_err;
 import aux::stmt_to_ann;
 import aux::log_states;
 import aux::log_states_err;
@@ -63,9 +60,12 @@ import aux::path_to_ident;
 import aux::if_ty;
 import aux::if_check;
 import aux::plain_if;
+import aux::forget_in_poststate;
+import tritv::tritv_clone;
+import tritv::tritv_set;
+import tritv::ttrue;
 
 import bitvectors::seq_preconds;
-import bitvectors::union_postconds;
 import bitvectors::intersect_postconds;
 import bitvectors::declare_var;
 import bitvectors::bit_num;
@@ -193,8 +193,8 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
             alt (chk) {
                 case (if_check) {
                     let aux::constr c = expr_to_constr(fcx.ccx.tcx, antec);
-                    conseq_prestate = bitv::clone(conseq_prestate);
-                    bitv::set(conseq_prestate, bit_num(fcx, c.node), true);
+                    conseq_prestate = tritv_clone(conseq_prestate);
+                    tritv_set(bit_num(fcx, c.node), conseq_prestate, ttrue);
                 }
                 case (_) {}
             }
@@ -352,8 +352,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
             ret changed;
         }
         case (expr_move(?lhs, ?rhs)) {
-            // FIXME: this needs to deinitialize the rhs
-
+        
             extend_prestate_ann(fcx.ccx, e.id, pres);
             alt (lhs.node) {
                 case (expr_path(?p)) {
@@ -362,9 +361,8 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
                     changed = pure_exp(fcx.ccx, lhs.id, pres) || changed;
                     changed = find_pre_post_state_expr
                         (fcx, pres, rhs) || changed;
-                    changed = extend_poststate_ann
-                        (fcx.ccx, e.id, expr_poststate(fcx.ccx, rhs)) ||
-                        changed;
+                    // not extending e's poststate,
+                    // because rhs is getting deinit'd anyway
                     changed = gen_if_local(fcx, lhs.id, e.id, p) || changed;
                 }
                 case (_) {
@@ -381,6 +379,9 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
                         || changed;
                 }
             }
+
+            changed = forget_in_poststate(fcx, rhs.span, e.id, rhs.id)
+                || changed;
             ret changed;
         }
         case (expr_assign(?lhs, ?rhs)) {
@@ -725,25 +726,42 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
                                 find_pre_post_state_expr(fcx, pres,
                                                          an_init.expr)
                                 || changed;
-                            changed =
-                                extend_poststate(stmt_ann.states.poststate,
-                                                 expr_poststate(fcx.ccx,
-                                                                an_init.expr))
-                                    || changed;
+
+
+                            /* FIXME less copypasta */
+                            alt (an_init.op) {
+                                case (init_move) {
+                                    changed = forget_in_poststate(fcx,
+                                      an_init.expr.span, id, an_init.expr.id)
+                                        || changed;
+                /* Safe to forget rhs's poststate here 'cause it's a var. */
+                                }
+                                case (_) { /* nothing gets deinitialized */ 
+                                    changed =
+                                      extend_poststate(
+                                        stmt_ann.states.poststate,
+                                        expr_poststate(fcx.ccx, an_init.expr))
+                                        || changed;
+                                } 
+                            }
+
                             changed =
                                 gen_poststate(fcx, id,
                                               rec(id=alocal.node.id,
                                                   c=ninit(alocal.node.ident)))
                                 || changed;
-                            log "Summary: stmt = ";
-                            log_stmt(*s);
-                            log "prestate = ";
-                            log bitv::to_str(stmt_ann.states.prestate);
-                            log_bitv(fcx, stmt_ann.states.prestate);
-                            log "poststate =";
-                            log_bitv(fcx, stmt_ann.states.poststate);
-                            log "changed =";
-                            log changed;
+                            
+                            /*
+                            log_err "Summary: stmt = ";
+                            log_stmt_err(*s);
+                            log_err "prestate = ";
+                            log_tritv_err(fcx, stmt_ann.states.prestate);
+                            log_err "poststate =";
+                            log_tritv_err(fcx, stmt_ann.states.poststate);
+                            log_err "changed =";
+                            log_err changed;
+                            */
+
                             ret changed;
                         }
                         case (none) {
@@ -778,17 +796,18 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
             changed =
                 extend_poststate(stmt_ann.states.poststate,
                                  expr_poststate(fcx.ccx, ex)) || changed;
+            
             /*
-              log("Summary: stmt = ");
-              log_stmt(*s);
-              log("prestate = ");
-              log(bitv::to_str(stmt_ann.states.prestate));
-              log_bitv(enclosing, stmt_ann.states.prestate);
-              log("poststate =");
-              log(bitv::to_str(stmt_ann.states.poststate));
-              log_bitv(enclosing, stmt_ann.states.poststate);
-              log("changed =");
-              log(changed);
+              log_err("Summary: stmt = ");
+              log_stmt_err(*s);
+              log_err("prestate = ");
+              //              log_err(bitv::to_str(stmt_ann.states.prestate));
+              log_tritv_err(fcx, stmt_ann.states.prestate);
+              log_err("poststate =");
+              //   log_err(bitv::to_str(stmt_ann.states.poststate));
+              log_tritv_err(fcx, stmt_ann.states.poststate);
+              log_err("changed =");
+              log_err(changed);
             */
 
             ret changed;
@@ -833,9 +852,9 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b) ->
     log_err "poststate = ";
     log_states_err(block_states(fcx.ccx, b));
     log_err "pres0:";
-    log_bitv_err(fcx, pres0);
+    log_tritv_err(fcx, pres0);
     log_err "post:";
-    log_bitv_err(fcx, post);
+    log_tritv_err(fcx, post);
     */
 
     ret changed;
@@ -844,7 +863,7 @@ 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);
     auto changed =
-        find_pre_post_state_block(fcx, empty_prestate(num_local_vars),
+        find_pre_post_state_block(fcx, block_prestate(fcx.ccx, f.body),
                                   f.body);
     // Treat the tail expression as a return statement
 
diff --git a/src/comp/middle/tstate/tritv.rs b/src/comp/middle/tstate/tritv.rs
new file mode 100644
index 000000000000..bf4a08ad9863
--- /dev/null
+++ b/src/comp/middle/tstate/tritv.rs
@@ -0,0 +1,246 @@
+import std::bitv;
+
+export t;
+export create_tritv;
+export tritv_clone;
+export tritv_set;
+export to_vec;
+export trit;
+export dont_care;
+export ttrue;
+export tfalse;
+export tritv_get;
+export tritv_set_all;
+export tritv_difference;
+export tritv_union;
+export tritv_intersect;
+export tritv_copy;
+export tritv_clear;
+export tritv_doesntcare;
+
+/* for a fixed index: 
+   10 = "this constraint may or may not be true after execution"
+   01 = "this constraint is definitely true"
+   00 = "this constraint is definitely false"
+   11 should never appear
+ FIXME: typestate precondition (uncertain and val must
+ have the same length; 11 should never appear in a given position)
+*/
+
+type t = rec(bitv::t uncertain, bitv::t val, uint nbits);
+tag trit {
+    ttrue;
+    tfalse;
+    dont_care;
+}
+
+fn create_tritv(uint len) -> t {
+  ret rec(uncertain=bitv::create(len, true),
+          val=bitv::create(len, false),
+          nbits=len);
+}
+
+
+fn trit_minus(trit a, trit b) -> trit {
+    /*   2 - anything = 2
+         1 - 1 = 2
+         1 - 0 is an error
+         1 - 2 = 1
+         0 - 1 is an error
+         0 - anything else - 0
+     */
+  alt (a) {
+    case (dont_care) { dont_care }
+    case (ttrue) {
+      alt (b) {
+        case (ttrue)     { dont_care }
+        case (tfalse)    { ttrue } /* internally contradictory, but
+                                      I guess it'll get flagged? */
+        case (dont_care) { ttrue }
+      }
+    }
+    case (tfalse) {
+      alt (b) {
+        case (ttrue) { tfalse } /* see above comment */
+        case (_)     { tfalse }
+      }
+    }
+  }
+}
+
+fn trit_or(trit a, trit b) -> trit {
+  alt (a) {
+    case (dont_care) { b }
+    case (ttrue)     { ttrue }
+    case (tfalse)    {
+      alt (b) {
+        case (ttrue)  { dont_care } /* FIXME: ?????? */
+        case (_)      { tfalse }
+      }
+    }
+  }
+}
+
+// FIXME: not sure about this
+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)    { tfalse } // FIXME: ???
+      }
+    }
+    case (tfalse) { tfalse }
+  }
+}
+
+fn tritv_difference(&t p1, &t p2) -> bool {
+    let uint i = 0u;
+    assert (p1.nbits == p2.nbits);
+    let uint sz = p1.nbits;
+    auto changed = false;
+    while (i < sz) {
+      auto old = tritv_get(p1, i);
+      auto new = trit_minus(old, tritv_get(p2, i));
+      changed = changed || (old != new);
+      tritv_set(i, p1, new);
+      i += 1u;
+    }
+    ret changed;
+}
+
+fn tritv_union(&t p1, &t p2) -> bool {
+    let uint i = 0u;
+    assert (p1.nbits == p2.nbits);
+    let uint sz = p1.nbits;
+    auto changed = false;
+    while (i < sz) {
+      auto old = tritv_get(p1, i);
+      auto new = trit_or(old, tritv_get(p2, i));
+      changed = changed || (old != new);
+      tritv_set(i, p1, new);
+      i += 1u;
+    }
+    ret changed;
+}
+
+fn tritv_intersect(&t p1, &t p2) -> bool {
+    let uint i = 0u;
+    assert (p1.nbits == p2.nbits);
+    let uint sz = p1.nbits;
+    auto changed = false;
+    while (i < sz) {
+      auto old = tritv_get(p1, i);
+      auto new = trit_and(old, tritv_get(p2, i));
+      changed = changed || (old != new);
+      tritv_set(i, p1, new);
+      i += 1u;
+    }
+    ret changed;
+}
+
+fn tritv_get(&t v, uint i) -> trit {
+  auto b1 = bitv::get(v.uncertain, i);
+  auto b2 = bitv::get(v.val, i);
+  assert (! (b1 && b2));
+  if (b1)      { dont_care }
+  else if (b2) { ttrue }
+  else         { tfalse}
+}
+ 
+fn tritv_set(uint i, &t v, trit t) -> bool {
+  auto old = tritv_get(v, i);
+  alt (t) {
+    case (dont_care) {
+      bitv::set(v.uncertain, i, true);
+      bitv::set(v.val, i, false);
+    }
+    case (ttrue) {
+      bitv::set(v.uncertain, i, false);
+      bitv::set(v.val, i, true);
+    }
+    case (tfalse) {
+      bitv::set(v.uncertain, i, false);
+      bitv::set(v.val, i, false);
+    }
+  }
+  ret (old != t);
+}
+
+fn tritv_copy(&t target, &t source) -> bool {
+  let uint i = 0u;
+  assert (target.nbits == source.nbits);
+  auto changed = false;
+  auto old;
+  auto new;
+  while (i < target.nbits) {
+    old = bitv::get(target.uncertain, i);
+    new = bitv::get(source.uncertain, i);
+    bitv::set(target.uncertain, i, new);
+    changed = changed || (old != new);
+    old = bitv::get(target.val, i);
+    new = bitv::get(source.val, i);
+    bitv::set(target.val, i, new);
+    changed = changed || (old != new);
+    i += 1u;
+  }
+  ret changed;
+}
+
+fn tritv_set_all(&t v) {
+  let uint i = 0u;
+  while (i < v.nbits) {
+    tritv_set(i, v, ttrue);
+    i += 1u;
+  }
+}
+
+fn tritv_clear(&t v) {
+  let uint i = 0u;
+  while (i < v.nbits) {
+    tritv_set(i, v, dont_care);
+    i += 1u;
+  }
+}
+
+fn tritv_clone(&t v) -> t {
+  ret rec(uncertain=bitv::clone(v.uncertain),
+          val=bitv::clone(v.val),
+          nbits=v.nbits);
+}
+
+fn tritv_doesntcare(&t v) -> bool {
+  let uint i = 0u;
+  while (i < v.nbits) {
+    if (tritv_get(v, i) != dont_care) {
+      ret false;
+    }
+    i += 1u;
+  }
+  ret true;
+}
+
+fn to_vec(&t v) -> vec[uint] {
+  let uint i = 0u;
+  let vec[uint] res = [];
+  while (i < v.nbits) {
+    res += [alt (tritv_get(v, i)) {
+        case (dont_care) { 2u }
+        case (ttrue)     { 1u }
+        case (tfalse)    { 0u } }];
+    i += 1u;
+  }
+  ret res;
+}
+//
+// Local Variables:
+// mode: rust
+// fill-column: 78;
+// indent-tabs-mode: nil
+// c-basic-offset: 4
+// buffer-file-coding-system: utf-8-unix
+// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
+// End:
+//
diff --git a/src/comp/rustc.rc b/src/comp/rustc.rc
index 565b436d4045..3a96e03f0c51 100644
--- a/src/comp/rustc.rc
+++ b/src/comp/rustc.rc
@@ -33,6 +33,7 @@ mod middle {
         mod pre_post_conditions;
         mod states;
         mod ann;
+        mod tritv;
     }
 }
 
diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs
index 801dda99de4c..87a1908f8e06 100644
--- a/src/comp/util/common.rs
+++ b/src/comp/util/common.rs
@@ -252,6 +252,15 @@ fn is_hex_digit(char c) -> bool {
 }
 
 fn is_bin_digit(char c) -> bool { ret c == '0' || c == '1'; }
+
+// FIXME move to vec
+fn any[T](&fn(&T) -> bool f, &vec[T] v) -> bool {
+    for (T t in v) {
+        if (f(t)) { ret true; } 
+    }
+    ret false;
+}
+
 //
 // Local Variables:
 // mode: rust
diff --git a/src/test/compile-fail/use-after-move.rs b/src/test/compile-fail/use-after-move.rs
new file mode 100644
index 000000000000..6c26279c581a
--- /dev/null
+++ b/src/test/compile-fail/use-after-move.rs
@@ -0,0 +1,6 @@
+// error-pattern: Unsatisfied precondition constraint (for example, init(x
+fn main() {
+  auto x = @5;
+  auto y <- x;
+  log *x;
+}
\ No newline at end of file