# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1271164672 14400
# Node ID 8768145eed1ec0e0a6ee9b6ef2777d77a60bddc2
# Parent  a2cd6664f57fb30148c37dd0fb3020adc26d476b
Havoc relations that have been updated

diff -r a2cd6664f57f -r 8768145eed1e src/iflow.sml
--- 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)