diff --git a/Source/DafnyCore/DafnyPrelude.bpl b/Source/DafnyCore/DafnyPrelude.bpl
index 43259bb02d7..f1009b7163e 100644
--- a/Source/DafnyCore/DafnyPrelude.bpl
+++ b/Source/DafnyCore/DafnyPrelude.bpl
@@ -7,8 +7,9 @@
 // Copyright by the contributors to the Dafny Project
 // SPDX-License-Identifier: MIT
 
-const $$Language$Dafny: bool;  // To be recognizable to the ModelViewer as
-axiom $$Language$Dafny;        // coming from a Dafny program.
+const $$Language$Dafny: bool uses {  // To be recognizable to the ModelViewer as
+  axiom $$Language$Dafny;            // coming from a Dafny program.
+}
 
 // ---------------------------------------------------------------
 // -- Types ------------------------------------------------------
@@ -33,35 +34,35 @@ const unique TORDINAL  : Ty uses {
   axiom Tag(TORDINAL) == TagORDINAL;
 }
 // See for which axioms we can make use of the trigger to determine the connection.
-function TBitvector(int) : Ty uses {
-  axiom (forall w: int :: { TBitvector(w) } Inv0_TBitvector(TBitvector(w)) == w);
-}
-function TSet(Ty)      : Ty uses {
-  axiom (forall t: Ty :: { TSet(t) } Inv0_TSet(TSet(t)) == t);
-  axiom (forall t: Ty    :: { TSet(t) }      Tag(TSet(t))      == TagSet);
-}
-function TISet(Ty)     : Ty uses {
-  axiom (forall t: Ty :: { TISet(t) } Inv0_TISet(TISet(t)) == t);
-  axiom (forall t: Ty    :: { TISet(t) }     Tag(TISet(t))     == TagISet);
-}
-function TMultiSet(Ty) : Ty uses {
-  axiom (forall t: Ty :: { TMultiSet(t) } Inv0_TMultiSet(TMultiSet(t)) == t);
-  axiom (forall t: Ty    :: { TMultiSet(t) } Tag(TMultiSet(t)) == TagMultiSet);
-}
-function TSeq(Ty)      : Ty uses {
-  axiom (forall t: Ty :: { TSeq(t) } Inv0_TSeq(TSeq(t)) == t);
-  axiom (forall t: Ty    :: { TSeq(t) }      Tag(TSeq(t))      == TagSeq);
-}
-function TMap(Ty, Ty)  : Ty uses {
-  axiom (forall t, u: Ty :: { TMap(t,u) } Inv0_TMap(TMap(t,u)) == t);
-  axiom (forall t, u: Ty :: { TMap(t,u) } Inv1_TMap(TMap(t,u)) == u);
-  axiom (forall t, u: Ty :: { TMap(t,u) }    Tag(TMap(t,u))    == TagMap);
-}
-function TIMap(Ty, Ty) : Ty uses {
-  axiom (forall t, u: Ty :: { TIMap(t,u) } Inv0_TIMap(TIMap(t,u)) == t);
-  axiom (forall t, u: Ty :: { TIMap(t,u) } Inv1_TIMap(TIMap(t,u)) == u);
-  axiom (forall t, u: Ty :: { TIMap(t,u) }   Tag(TIMap(t,u))   == TagIMap);
-}
+function TBitvector(int) : Ty;
+axiom (forall w: int :: { TBitvector(w) } Inv0_TBitvector(TBitvector(w)) == w);
+
+function TSet(Ty) : Ty;
+axiom (forall t: Ty :: { TSet(t) } Inv0_TSet(TSet(t)) == t);
+axiom (forall t: Ty :: { TSet(t) }      Tag(TSet(t))      == TagSet);
+
+function TISet(Ty) : Ty;
+axiom (forall t: Ty :: { TISet(t) } Inv0_TISet(TISet(t)) == t);
+axiom (forall t: Ty :: { TISet(t) }     Tag(TISet(t))     == TagISet);
+
+function TMultiSet(Ty) : Ty;
+axiom (forall t: Ty :: { TMultiSet(t) } Inv0_TMultiSet(TMultiSet(t)) == t);
+axiom (forall t: Ty :: { TMultiSet(t) } Tag(TMultiSet(t)) == TagMultiSet);
+
+function TSeq(Ty) : Ty;
+axiom (forall t: Ty :: { TSeq(t) } Inv0_TSeq(TSeq(t)) == t);
+axiom (forall t: Ty :: { TSeq(t) } Tag(TSeq(t)) == TagSeq);
+
+function TMap(Ty, Ty) : Ty;
+axiom (forall t, u: Ty :: { TMap(t,u) } Inv0_TMap(TMap(t,u)) == t);
+axiom (forall t, u: Ty :: { TMap(t,u) } Inv1_TMap(TMap(t,u)) == u);
+axiom (forall t, u: Ty :: { TMap(t,u) } Tag(TMap(t,u)) == TagMap);
+
+function TIMap(Ty, Ty) : Ty;
+axiom (forall t, u: Ty :: { TIMap(t,u) } Inv0_TIMap(TIMap(t,u)) == t);
+axiom (forall t, u: Ty :: { TIMap(t,u) } Inv1_TIMap(TIMap(t,u)) == u);
+axiom (forall t, u: Ty :: { TIMap(t,u) } Tag(TIMap(t,u)) == TagIMap);
+
 
 function Inv0_TBitvector(Ty) : int;
 function Inv0_TSet(Ty) : Ty;
@@ -98,19 +99,17 @@ function TagFamily(Ty): TyTagFamily;
 // ---------------------------------------------------------------
 // -- Literals ---------------------------------------------------
 // ---------------------------------------------------------------
-function {:identity} Lit<T>(x: T): T { x } uses {
-  axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) );
-}
+function {:identity} Lit<T>(x: T): T { x }
+axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) );
 
 // Specialize Lit to concrete types.
 // These aren't logically required, but on some examples improve
 // verification speed
-function {:identity} LitInt(x: int): int { x } uses {
-  axiom (forall x: int :: { $Box(LitInt(x)) } $Box(LitInt(x)) == Lit($Box(x)) );
-}
-function {:identity} LitReal(x: real): real { x } uses {
-  axiom (forall x: real :: { $Box(LitReal(x)) } $Box(LitReal(x)) == Lit($Box(x)) );
-}
+function {:identity} LitInt(x: int): int { x }
+axiom (forall x: int :: { $Box(LitInt(x)) } $Box(LitInt(x)) == Lit($Box(x)) );
+
+function {:identity} LitReal(x: real): real { x }
+axiom (forall x: real :: { $Box(LitReal(x)) } $Box(LitReal(x)) == Lit($Box(x)) );
 
 // ---------------------------------------------------------------
 // -- Characters -------------------------------------------------
@@ -128,29 +127,26 @@ function {:inline} char#IsChar(n: int): bool {
 #endif
 
 type char;
-function char#FromInt(int): char uses {
-  axiom (forall n: int ::
-    { char#FromInt(n) }
-    char#IsChar(n) ==> char#ToInt(char#FromInt(n)) == n);
-}
-
-function char#ToInt(char): int uses {
-  axiom (forall ch: char ::
-    { char#ToInt(ch) }
-    char#FromInt(char#ToInt(ch)) == ch &&
-    char#IsChar(char#ToInt(ch)));
-}  
-
-function char#Plus(char, char): char uses {
-  axiom (forall a: char, b: char ::
-    { char#Plus(a, b) }
-    char#Plus(a, b) == char#FromInt(char#ToInt(a) + char#ToInt(b)));
-}
-function char#Minus(char, char): char uses {
-  axiom (forall a: char, b: char ::
-    { char#Minus(a, b) }
-    char#Minus(a, b) == char#FromInt(char#ToInt(a) - char#ToInt(b)));
-}
+function char#FromInt(int): char;
+axiom (forall n: int ::
+  { char#FromInt(n) }
+  char#IsChar(n) ==> char#ToInt(char#FromInt(n)) == n);
+
+function char#ToInt(char): int;
+axiom (forall ch: char ::
+  { char#ToInt(ch) }
+  char#FromInt(char#ToInt(ch)) == ch &&
+  char#IsChar(char#ToInt(ch)));
+
+function char#Plus(char, char): char;
+axiom (forall a: char, b: char ::
+  { char#Plus(a, b) }
+  char#Plus(a, b) == char#FromInt(char#ToInt(a) + char#ToInt(b)));
+
+function char#Minus(char, char): char;
+axiom (forall a: char, b: char ::
+  { char#Minus(a, b) }
+  char#Minus(a, b) == char#FromInt(char#ToInt(a) - char#ToInt(b)));
 
 // ---------------------------------------------------------------
 // -- References -------------------------------------------------
@@ -166,10 +162,9 @@ const null: ref;
 type Box;
 const $ArbitraryBoxValue: Box;
 
-function $Box<T>(T): Box uses {
-  axiom (forall<T> x : T :: { $Box(x) } $Unbox($Box(x)) == x);
-}
+function $Box<T>(T): Box;
 function $Unbox<T>(Box): T;
+axiom (forall<T> x : T :: { $Box(x) } $Unbox($Box(x)) == x);
 
 // Corresponding entries for boxes...
 // This could probably be solved by having Box also inhabit Ty
@@ -227,118 +222,117 @@ axiom (forall<T> v : T, t : Ty, h : Heap ::
 
 // Type-argument to $Is is the /representation type/,
 // the second value argument to $Is is the actual type.
-function $Is<T>(T,Ty): bool uses {           // no heap for now
-    axiom(forall v : int  :: { $Is(v,TInt) }  $Is(v,TInt));
-    axiom(forall v : real :: { $Is(v,TReal) } $Is(v,TReal));
-    axiom(forall v : bool :: { $Is(v,TBool) } $Is(v,TBool));
-    axiom(forall v : char :: { $Is(v,TChar) } $Is(v,TChar));
-    axiom(forall v : ORDINAL :: { $Is(v,TORDINAL) } $Is(v,TORDINAL));
-    
-    // Since every bitvector type is a separate type in Boogie, the $Is/$IsAlloc axioms
-    // for bitvectors are generated programatically. Except, TBitvector(0) is given here.
-    axiom (forall v: Bv0 :: { $Is(v, TBitvector(0)) } $Is(v, TBitvector(0)));
-
-    axiom (forall v: Set Box, t0: Ty :: { $Is(v, TSet(t0)) }
-      $Is(v, TSet(t0)) <==>
-      (forall bx: Box :: { v[bx] }
-        v[bx] ==> $IsBox(bx, t0)));
-    axiom (forall v: ISet Box, t0: Ty :: { $Is(v, TISet(t0)) }
-      $Is(v, TISet(t0)) <==>
-      (forall bx: Box :: { v[bx] }
-        v[bx] ==> $IsBox(bx, t0)));
-    axiom (forall v: MultiSet Box, t0: Ty :: { $Is(v, TMultiSet(t0)) }
-      $Is(v, TMultiSet(t0)) <==>
-      (forall bx: Box :: { v[bx] }
-        0 < v[bx] ==> $IsBox(bx, t0)));
-    axiom (forall v: MultiSet Box, t0: Ty :: { $Is(v, TMultiSet(t0)) }
-      $Is(v, TMultiSet(t0)) ==> $IsGoodMultiSet(v));
-    axiom (forall v: Seq Box, t0: Ty :: { $Is(v, TSeq(t0)) }
-      $Is(v, TSeq(t0)) <==>
-      (forall i : int :: { Seq#Index(v, i) }
-        0 <= i && i < Seq#Length(v) ==>
-        $IsBox(Seq#Index(v, i), t0)));
-        
-    axiom (forall v: Map Box Box, t0: Ty, t1: Ty ::
-      { $Is(v, TMap(t0, t1)) }
-      $Is(v, TMap(t0, t1))
-         <==> (forall bx: Box ::
-          { Map#Elements(v)[bx] } { Map#Domain(v)[bx] }
-          Map#Domain(v)[bx] ==>
-            $IsBox(Map#Elements(v)[bx], t1) &&
-            $IsBox(bx, t0)));
+function $Is<T>(T,Ty): bool;           // no heap for now
+axiom(forall v : int  :: { $Is(v,TInt) }  $Is(v,TInt));
+axiom(forall v : real :: { $Is(v,TReal) } $Is(v,TReal));
+axiom(forall v : bool :: { $Is(v,TBool) } $Is(v,TBool));
+axiom(forall v : char :: { $Is(v,TChar) } $Is(v,TChar));
+axiom(forall v : ORDINAL :: { $Is(v,TORDINAL) } $Is(v,TORDINAL));
+
+// Since every bitvector type is a separate type in Boogie, the $Is/$IsAlloc axioms
+// for bitvectors are generated programatically. Except, TBitvector(0) is given here.
+axiom (forall v: Bv0 :: { $Is(v, TBitvector(0)) } $Is(v, TBitvector(0)));
+
+axiom (forall v: Set Box, t0: Ty :: { $Is(v, TSet(t0)) }
+  $Is(v, TSet(t0)) <==>
+  (forall bx: Box :: { v[bx] }
+    v[bx] ==> $IsBox(bx, t0)));
+axiom (forall v: ISet Box, t0: Ty :: { $Is(v, TISet(t0)) }
+  $Is(v, TISet(t0)) <==>
+  (forall bx: Box :: { v[bx] }
+    v[bx] ==> $IsBox(bx, t0)));
+axiom (forall v: MultiSet Box, t0: Ty :: { $Is(v, TMultiSet(t0)) }
+  $Is(v, TMultiSet(t0)) <==>
+  (forall bx: Box :: { v[bx] }
+    0 < v[bx] ==> $IsBox(bx, t0)));
+axiom (forall v: MultiSet Box, t0: Ty :: { $Is(v, TMultiSet(t0)) }
+  $Is(v, TMultiSet(t0)) ==> $IsGoodMultiSet(v));
+axiom (forall v: Seq Box, t0: Ty :: { $Is(v, TSeq(t0)) }
+  $Is(v, TSeq(t0)) <==>
+  (forall i : int :: { Seq#Index(v, i) }
+    0 <= i && i < Seq#Length(v) ==>
+    $IsBox(Seq#Index(v, i), t0)));
+
+axiom (forall v: Map Box Box, t0: Ty, t1: Ty ::
+  { $Is(v, TMap(t0, t1)) }
+  $Is(v, TMap(t0, t1))
+     <==> (forall bx: Box ::
+      { Map#Elements(v)[bx] } { Map#Domain(v)[bx] }
+      Map#Domain(v)[bx] ==>
+        $IsBox(Map#Elements(v)[bx], t1) &&
+        $IsBox(bx, t0)));
             
-    axiom (forall v: Map Box Box, t0: Ty, t1: Ty ::
-      { $Is(v, TMap(t0, t1)) }
-      $Is(v, TMap(t0, t1)) ==>
-        $Is(Map#Domain(v), TSet(t0)) &&
-        $Is(Map#Values(v), TSet(t1)) &&
-        $Is(Map#Items(v), TSet(Tclass._System.Tuple2(t0, t1))));
-    axiom (forall v: IMap Box Box, t0: Ty, t1: Ty ::
-      { $Is(v, TIMap(t0, t1)) }
-      $Is(v, TIMap(t0, t1))
-         <==> (forall bx: Box ::
-          { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] }
-          IMap#Domain(v)[bx] ==>
-            $IsBox(IMap#Elements(v)[bx], t1) &&
-            $IsBox(bx, t0)));
-    axiom (forall v: IMap Box Box, t0: Ty, t1: Ty ::
-      { $Is(v, TIMap(t0, t1)) }
-      $Is(v, TIMap(t0, t1)) ==>
-        $Is(IMap#Domain(v), TISet(t0)) &&
-        $Is(IMap#Values(v), TISet(t1)) &&
-        $Is(IMap#Items(v), TISet(Tclass._System.Tuple2(t0, t1))));
-}
-function $IsAlloc<T>(T,Ty,Heap): bool uses {
-    axiom(forall h : Heap, v : int  :: { $IsAlloc(v,TInt,h) }  $IsAlloc(v,TInt,h));
-    axiom(forall h : Heap, v : real :: { $IsAlloc(v,TReal,h) } $IsAlloc(v,TReal,h));
-    axiom(forall h : Heap, v : bool :: { $IsAlloc(v,TBool,h) } $IsAlloc(v,TBool,h));
-    axiom(forall h : Heap, v : char :: { $IsAlloc(v,TChar,h) } $IsAlloc(v,TChar,h));
-    axiom(forall h : Heap, v : ORDINAL :: { $IsAlloc(v,TORDINAL,h) } $IsAlloc(v,TORDINAL,h));
+axiom (forall v: Map Box Box, t0: Ty, t1: Ty ::
+  { $Is(v, TMap(t0, t1)) }
+  $Is(v, TMap(t0, t1)) ==>
+    $Is(Map#Domain(v), TSet(t0)) &&
+    $Is(Map#Values(v), TSet(t1)) &&
+    $Is(Map#Items(v), TSet(Tclass._System.Tuple2(t0, t1))));
+axiom (forall v: IMap Box Box, t0: Ty, t1: Ty ::
+  { $Is(v, TIMap(t0, t1)) }
+  $Is(v, TIMap(t0, t1))
+     <==> (forall bx: Box ::
+      { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] }
+      IMap#Domain(v)[bx] ==>
+        $IsBox(IMap#Elements(v)[bx], t1) &&
+        $IsBox(bx, t0)));
+axiom (forall v: IMap Box Box, t0: Ty, t1: Ty ::
+  { $Is(v, TIMap(t0, t1)) }
+  $Is(v, TIMap(t0, t1)) ==>
+    $Is(IMap#Domain(v), TISet(t0)) &&
+    $Is(IMap#Values(v), TISet(t1)) &&
+    $Is(IMap#Items(v), TISet(Tclass._System.Tuple2(t0, t1))));
+
+function $IsAlloc<T>(T,Ty,Heap): bool;
+axiom(forall h : Heap, v : int  :: { $IsAlloc(v,TInt,h) }  $IsAlloc(v,TInt,h));
+axiom(forall h : Heap, v : real :: { $IsAlloc(v,TReal,h) } $IsAlloc(v,TReal,h));
+axiom(forall h : Heap, v : bool :: { $IsAlloc(v,TBool,h) } $IsAlloc(v,TBool,h));
+axiom(forall h : Heap, v : char :: { $IsAlloc(v,TChar,h) } $IsAlloc(v,TChar,h));
+axiom(forall h : Heap, v : ORDINAL :: { $IsAlloc(v,TORDINAL,h) } $IsAlloc(v,TORDINAL,h));
     
-    axiom (forall v: Bv0, h: Heap :: { $IsAlloc(v, TBitvector(0), h) } $IsAlloc(v, TBitvector(0), h));
-    
-    axiom (forall v: Set Box, t0: Ty, h: Heap :: { $IsAlloc(v, TSet(t0), h) }
-      $IsAlloc(v, TSet(t0), h) <==>
-      (forall bx: Box :: { v[bx] }
-        v[bx] ==> $IsAllocBox(bx, t0, h)));
-    axiom (forall v: ISet Box, t0: Ty, h: Heap :: { $IsAlloc(v, TISet(t0), h) }
-      $IsAlloc(v, TISet(t0), h) <==>
-      (forall bx: Box :: { v[bx] }
-        v[bx] ==> $IsAllocBox(bx, t0, h)));
-    axiom (forall v: MultiSet Box, t0: Ty, h: Heap :: { $IsAlloc(v, TMultiSet(t0), h) }
-      $IsAlloc(v, TMultiSet(t0), h) <==>
-      (forall bx: Box :: { v[bx] }
-        0 < v[bx] ==> $IsAllocBox(bx, t0, h)));
-    axiom (forall v: Seq Box, t0: Ty, h: Heap :: { $IsAlloc(v, TSeq(t0), h) }
-      $IsAlloc(v, TSeq(t0), h) <==>
-      (forall i : int :: { Seq#Index(v, i) }
-        0 <= i && i < Seq#Length(v) ==>
-    	$IsAllocBox(Seq#Index(v, i), t0, h)));
-    	
-    axiom (forall v: Map Box Box, t0: Ty, t1: Ty, h: Heap ::
-      { $IsAlloc(v, TMap(t0, t1), h) }
-      $IsAlloc(v, TMap(t0, t1), h)
-         <==> (forall bx: Box ::
-          { Map#Elements(v)[bx] } { Map#Domain(v)[bx] }
-          Map#Domain(v)[bx] ==>
-            $IsAllocBox(Map#Elements(v)[bx], t1, h) &&
-            $IsAllocBox(bx, t0, h)));
-            
-    axiom (forall v: IMap Box Box, t0: Ty, t1: Ty, h: Heap ::
-      { $IsAlloc(v, TIMap(t0, t1), h) }
-      $IsAlloc(v, TIMap(t0, t1), h)
-         <==> (forall bx: Box ::
-          { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] }
-          IMap#Domain(v)[bx] ==>
-            $IsAllocBox(IMap#Elements(v)[bx], t1, h) &&
-            $IsAllocBox(bx, t0, h)));
-}
+axiom (forall v: Bv0, h: Heap :: { $IsAlloc(v, TBitvector(0), h) } $IsAlloc(v, TBitvector(0), h));
+ 
+axiom (forall v: Set Box, t0: Ty, h: Heap :: { $IsAlloc(v, TSet(t0), h) }
+  $IsAlloc(v, TSet(t0), h) <==>
+  (forall bx: Box :: { v[bx] }
+    v[bx] ==> $IsAllocBox(bx, t0, h)));
+axiom (forall v: ISet Box, t0: Ty, h: Heap :: { $IsAlloc(v, TISet(t0), h) }
+  $IsAlloc(v, TISet(t0), h) <==>
+  (forall bx: Box :: { v[bx] }
+    v[bx] ==> $IsAllocBox(bx, t0, h)));
+axiom (forall v: MultiSet Box, t0: Ty, h: Heap :: { $IsAlloc(v, TMultiSet(t0), h) }
+  $IsAlloc(v, TMultiSet(t0), h) <==>
+  (forall bx: Box :: { v[bx] }
+    0 < v[bx] ==> $IsAllocBox(bx, t0, h)));
+axiom (forall v: Seq Box, t0: Ty, h: Heap :: { $IsAlloc(v, TSeq(t0), h) }
+  $IsAlloc(v, TSeq(t0), h) <==>
+  (forall i : int :: { Seq#Index(v, i) }
+    0 <= i && i < Seq#Length(v) ==>
+	$IsAllocBox(Seq#Index(v, i), t0, h)));
+	
+axiom (forall v: Map Box Box, t0: Ty, t1: Ty, h: Heap ::
+  { $IsAlloc(v, TMap(t0, t1), h) }
+  $IsAlloc(v, TMap(t0, t1), h)
+     <==> (forall bx: Box ::
+      { Map#Elements(v)[bx] } { Map#Domain(v)[bx] }
+      Map#Domain(v)[bx] ==>
+        $IsAllocBox(Map#Elements(v)[bx], t1, h) &&
+        $IsAllocBox(bx, t0, h)));
+        
+axiom (forall v: IMap Box Box, t0: Ty, t1: Ty, h: Heap ::
+  { $IsAlloc(v, TIMap(t0, t1), h) }
+  $IsAlloc(v, TIMap(t0, t1), h)
+     <==> (forall bx: Box ::
+      { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] }
+      IMap#Domain(v)[bx] ==>
+        $IsAllocBox(IMap#Elements(v)[bx], t1, h) &&
+        $IsAllocBox(bx, t0, h)));
 
-function $AlwaysAllocated(Ty): bool uses {
-    axiom (forall ty: Ty :: { $AlwaysAllocated(ty) }
-      $AlwaysAllocated(ty) ==>
-      (forall h: Heap, v: Box  :: { $IsAllocBox(v, ty, h) }  $IsBox(v, ty) ==> $IsAllocBox(v, ty, h)));
-}
+
+function $AlwaysAllocated(Ty): bool;
+  axiom (forall ty: Ty :: { $AlwaysAllocated(ty) }
+    $AlwaysAllocated(ty) ==>
+    (forall h: Heap, v: Box  :: { $IsAllocBox(v, ty, h) }  $IsBox(v, ty) ==> $IsAllocBox(v, ty, h)));
 
 function $OlderTag(Heap): bool;
 
@@ -541,13 +535,12 @@ axiom (forall<T> cl : ClassName, nm: NameFamily ::
 
 function $IsGhostField<T>(Field T): bool uses {
    axiom $IsGhostField(alloc); // treat as ghost field, since it is allowed to be changed by ghost code
-  
-   axiom (forall h: Heap, k: Heap :: { $HeapSuccGhost(h,k) }
-      $HeapSuccGhost(h,k) ==>
-        $HeapSucc(h,k) &&
-        (forall<alpha> o: ref, f: Field alpha :: { read(k, o, f) }
-          !$IsGhostField(f) ==> read(h, o, f) == read(k, o, f)));
 }
+axiom (forall h: Heap, k: Heap :: { $HeapSuccGhost(h,k) }
+  $HeapSuccGhost(h,k) ==>
+    $HeapSucc(h,k) &&
+    (forall<alpha> o: ref, f: Field alpha :: { read(k, o, f) }
+      !$IsGhostField(f) ==> read(h, o, f) == read(k, o, f)));
 
 // ---------------------------------------------------------------
 // -- Allocatedness and Heap Succession --------------------------
@@ -572,9 +565,9 @@ const unique allocName: NameFamily;
 // -- Arrays -----------------------------------------------------
 // ---------------------------------------------------------------
 
-function _System.array.Length(a: ref): int uses {
-  axiom (forall o: ref :: 0 <= _System.array.Length(o));
-}
+function _System.array.Length(a: ref): int;
+axiom (forall o: ref :: {_System.array.Length(o)} 0 <= _System.array.Length(o));
+
 
 // ---------------------------------------------------------------
 // -- Reals ------------------------------------------------------
@@ -931,6 +924,7 @@ axiom (forall<T> s: Set T :: { MultiSet#Card(MultiSet#FromSet(s)) }
 function MultiSet#FromSeq<T>(Seq T): MultiSet T uses {
   axiom (forall<T> :: MultiSet#FromSeq(Seq#Empty(): Seq T) == MultiSet#Empty(): MultiSet T);
 }
+
 // conversion produces a good map.
 axiom (forall<T> s: Seq T :: { MultiSet#FromSeq(s) } $IsGoodMultiSet(MultiSet#FromSeq(s)) );
 // cardinality axiom
diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs
index 86edcc4ed16..6eadac8ff71 100644
--- a/Source/DafnyCore/Verifier/Translator.cs
+++ b/Source/DafnyCore/Verifier/Translator.cs
@@ -38,6 +38,17 @@ public partial class Translator {
     public bool UseOptimizationInZ3 { get; set; }
 
     void AddOtherDefinition(Bpl.Declaration declaration, Axiom axiom) {
+      sink.AddTopLevelDeclaration(axiom);
+
+      // Axioms that have triggers and bound variables do not need to be inside
+      // uses clauses. Putting such axioms inside uses clauses weakens pruning
+      // when the trigger contains more than one function or constant symbol combined.
+      // The early return would happen whenever axiom is of the form:
+      // axiom (<quantifier> <(optionally) type variables> <at least one dummy variable> :: { ... } ...
+      if (axiom.Expr is Microsoft.Boogie.QuantifierExpr qe && qe.Dummies != null && qe.Dummies.Any() &&
+          qe.Triggers != null && qe.Triggers.Tr != null && qe.Triggers.Tr.Any()) {
+        return;
+      }
 
       switch (declaration) {
         case null:
@@ -50,8 +61,6 @@ void AddOtherDefinition(Bpl.Declaration declaration, Axiom axiom) {
           break;
         default: throw new ArgumentException("Declaration must be a function or constant");
       }
-
-      sink.AddTopLevelDeclaration(axiom);
     }
 
     public class TranslatorFlags {
diff --git a/Test/dafny0/Fuel.dfy.expect b/Test/dafny0/Fuel.dfy.expect
index 27f7a49c9b7..7c73d419cf8 100755
--- a/Test/dafny0/Fuel.dfy.expect
+++ b/Test/dafny0/Fuel.dfy.expect
@@ -21,19 +21,19 @@ Fuel.dfy(324,21): Related location
 Fuel.dfy(313,41): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(312,43): Related location
+Fuel.dfy(314,72): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(312,58): Related location
+Fuel.dfy(314,93): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(314,46): Related location
+Fuel.dfy(312,43): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(314,72): Related location
+Fuel.dfy(312,58): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(314,93): Related location
+Fuel.dfy(314,46): Related location
 Fuel.dfy(335,49): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple'
 Fuel.dfy(335,50): Error: index out of range
 Fuel.dfy(336,38): Error: index out of range
@@ -46,7 +46,7 @@ Fuel.dfy(329,21): Related location
 Fuel.dfy(313,41): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(312,43): Related location
+Fuel.dfy(312,58): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
 Fuel.dfy(314,72): Related location
@@ -55,7 +55,7 @@ Fuel.dfy(329,21): Related location
 Fuel.dfy(314,93): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(312,58): Related location
+Fuel.dfy(312,43): Related location
 Fuel.dfy(336,71): Error: index out of range
 Fuel.dfy(397,22): Error: assertion might not hold
 Fuel.dfy(398,22): Error: assertion might not hold
diff --git a/Test/dafny4/NipkowKlein-chapter7.dfy b/Test/dafny4/NipkowKlein-chapter7.dfy
index 60ae262da83..f6c3ae0eb07 100644
--- a/Test/dafny4/NipkowKlein-chapter7.dfy
+++ b/Test/dafny4/NipkowKlein-chapter7.dfy
@@ -240,6 +240,7 @@ least lemma star_transitive_aux(c0: com, s0: state, c1: com, s1: state, c2: com,
   requires small_step_star(c0, s0, c1, s1)
   ensures small_step_star(c1, s1, c2, s2) ==> small_step_star(c0, s0, c2, s2)
 {
+  if small_step_star(c1, s1, c2, s2) {}
 }
 
 // The big-step semantics can be simulated by some number of small steps
diff --git a/Test/git-issues/git-issue-2026.dfy.expect b/Test/git-issues/git-issue-2026.dfy.expect
index d9a38be0bce..191893e6a72 100644
--- a/Test/git-issues/git-issue-2026.dfy.expect
+++ b/Test/git-issues/git-issue-2026.dfy.expect
@@ -8,25 +8,25 @@ git-issue-2026.dfy(12,0): initial state:
 	ret : _System.array<seq<char>> = ()
 git-issue-2026.dfy(13,24):
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 39)] := @0, [0] := @0)
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
 	@0 : seq<char> = ['o', 'd', 'd']
 git-issue-2026.dfy(15,14):
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 39)] := @0, [0] := @0)
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
 	i : int = 0
 	@0 : seq<char> = ['o', 'd', 'd']
 git-issue-2026.dfy(16,4): after some loop iterations:
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 39)] := @0)
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0)
 	i : int = 0
 	@0 : seq<char> = ['o', 'd', 'd']
 git-issue-2026.dfy(22,27):
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 39)] := @0, [0] := @0)
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
 	i : int = 0
 	@0 : seq<char> = ['o', 'd', 'd']
 git-issue-2026.dfy(26,18):
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 39)] := @0, [0] := @0)
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
 	i : int = 1
 	@0 : seq<char> = ['o', 'd', 'd']
diff --git a/Test/git-issues/git-issue-2299.dfy.expect b/Test/git-issues/git-issue-2299.dfy.expect
index 319e0e2fb07..2c938effc18 100644
--- a/Test/git-issues/git-issue-2299.dfy.expect
+++ b/Test/git-issues/git-issue-2299.dfy.expect
@@ -7,13 +7,13 @@ git-issue-2299.dfy(21,4): Related location
 git-issue-2299.dfy(67,13): Error: assertion might not hold
 git-issue-2299.dfy(21,4): Related location
 git-issue-2299.dfy(81,11): Error: assertion might not hold
-git-issue-2299.dfy(27,18): Related location
-git-issue-2299.dfy(16,4): Related location
+git-issue-2299.dfy(27,4): Related location
+git-issue-2299.dfy(10,11): Related location
 git-issue-2299.dfy(81,11): Error: assertion might not hold
 git-issue-2299.dfy(27,32): Related location
 git-issue-2299.dfy(21,4): Related location
 git-issue-2299.dfy(81,11): Error: assertion might not hold
-git-issue-2299.dfy(27,4): Related location
-git-issue-2299.dfy(10,11): Related location
+git-issue-2299.dfy(27,18): Related location
+git-issue-2299.dfy(16,4): Related location
 
 Dafny program verifier finished with 7 verified, 7 errors
diff --git a/Test/git-issues/git-issue-3855.dfy b/Test/git-issues/git-issue-3855.dfy
index 5839defe290..dec9da7cfad 100644
--- a/Test/git-issues/git-issue-3855.dfy
+++ b/Test/git-issues/git-issue-3855.dfy
@@ -666,26 +666,26 @@ method {:rlimit 30000} {:vcs_split_on_every_assert} fNullify(o : Object, f : str
   
       var nedge :=  Edge(o,f, o.fields[f]); //edge to be nullified
 
-      assert nedge in edges(objects);
+      //assert nedge in edges(objects);
 
       o.fields := RemoveKey(o.fields,f);
 
-      assert nedge !in edges(objects);
+      //assert nedge !in edges(objects);
 
       var zedges := edges(objects); 
 
-      assert zedges + {nedge} == xedges;
+      //assert zedges + {nedge} == xedges;
 
       RefCountIsMonotonic(xisos,xedges,zedges);
 
-      assert heapExternalsZeroOrOneEdges(xedges);
-      assert zedges <= xedges;
-      assert justHeapExternalEdges(zedges) <= justHeapExternalEdges(xedges);
-      assert (set he <- justHeapExternalEdges(zedges) :: he.t.region) <= 
-             (set he <- justHeapExternalEdges(xedges) :: he.t.region);
-      assert forall r <- allRegions(old(objects)) ::
-             externalEdges(r, justHeapExternalEdges(zedges)) <= 
-             externalEdges(r, justHeapExternalEdges(xedges));
+      //assert heapExternalsZeroOrOneEdges(xedges);
+      //assert zedges <= xedges;
+      //assert justHeapExternalEdges(zedges) <= justHeapExternalEdges(xedges);
+      //assert (set he <- justHeapExternalEdges(zedges) :: he.t.region) <= 
+      //       (set he <- justHeapExternalEdges(xedges) :: he.t.region);
+      //assert forall r <- allRegions(old(objects)) ::
+      //       externalEdges(r, justHeapExternalEdges(zedges)) <= 
+      //       externalEdges(r, justHeapExternalEdges(xedges));
 
       assert heapExternalsZeroOrOneEdges(xedges);