--- a/src/iflow.sml	Sun Apr 11 17:55:37 2010 -0400
+++ b/src/iflow.sml	Tue Apr 13 09:17:52 2010 -0400
@@ -1984,6 +1984,21 @@
 
 end
 
+fun havocReln r =
+    let
+        fun hr p =
+            case p of
+                True => p
+              | False => p
+              | Unknown => p
+              | And (p1, p2) => And (hr p1, hr p2)
+              | Or (p1, p2) => Or (hr p1, hr p2)
+              | Reln (r', _) => if r' = r then True else p
+              | Cond (e, p) => Cond (e, hr p)
+    in
+        hr
+    end
+
 fun evalExp env (e as (_, loc), st) =
     let
         fun default () =
@@ -2259,6 +2274,8 @@
                          val p = And (p,
                                       And (Reln (Sql "$Old", [Var old]),
                                            Reln (Sql tab, [Var old])))
+
+                         val st = St.setAmbient (st, havocReln (Sql tab) (St.ambient st))
                      in
                          (Recd [], St.addDelete (st, (loc, And (St.ambient st, p))))
                      end
@@ -2308,6 +2325,8 @@
                                       And (Reln (Sql (tab ^ "$New"), [Recd fs]),
                                            And (Reln (Sql "$Old", [Var old]),
                                                 Reln (Sql tab, [Var old]))))
+
+                         val st = St.setAmbient (st, havocReln (Sql tab) (St.ambient st))
                      in
                          (Recd [], St.addUpdate (st, (loc, And (St.ambient st, p))))
                      end)