From a48f2cc95e01742e8d1a6c3e69846598ee2a91a2 Mon Sep 17 00:00:00 2001
From: Unknown <qadeer@GHALIB.redmond.corp.microsoft.com>
Date: Wed, 18 May 2011 23:25:29 -0700
Subject: fixed the axiom about TypeOf

---
 BCT/BytecodeTranslator/Heap.cs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'BCT')

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 28964c15..87d950c4 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -60,7 +60,8 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
 {
   $result := $TypeOf($DynamicType(this));
 }
-axiom (forall t: Type :: $DynamicType($TypeOf(t)) == t);
+function $TypeOfInv(Ref): Type;
+axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);
 
 function $ThreadDelegate(Ref) : Ref;
 
@@ -226,7 +227,8 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
 {
   $result := $TypeOf($DynamicType(this));
 }
-axiom (forall t: Type :: $DynamicType($TypeOf(t)) == t);
+function $TypeOfInv(Ref): Type;
+axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);
 
 function $ThreadDelegate(Ref) : Ref;
 procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
-- 
cgit v1.2.3