diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy
index 8b9e73f15f..15672db94f 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy
@@ -134,6 +134,12 @@ method DefiniteAssignment()
     }
   }
   target := z;
+
+  var q: int; 
+  opaque
+    ensures q == 3
+  {
+  } 
 }
 
 method EnsuresDoesNotHold() {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy.expect
index c6eaab54b1..abc13bad8d 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy.expect
@@ -9,8 +9,10 @@ opaqueBlock.dfy(93,2): Error: opaque block might violate context's modifies clau
 opaqueBlock.dfy(106,4): Error: opaque block might violate context's modifies clause
 opaqueBlock.dfy(127,12): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here
 opaqueBlock.dfy(130,17): Error: variable 'z', which is subject to definite-assignment rules, might be uninitialized here
-opaqueBlock.dfy(142,12): Error: ensures might not hold
-opaqueBlock.dfy(206,6): Error: assignment might update an object not in the enclosing context's modifies clause
-opaqueBlock.dfy(218,2): Error: assertion might not hold
+opaqueBlock.dfy(140,12): Error: variable 'q', which is subject to definite-assignment rules, might be uninitialized here
+opaqueBlock.dfy(140,14): Error: ensures might not hold
+opaqueBlock.dfy(148,12): Error: ensures might not hold
+opaqueBlock.dfy(212,6): Error: assignment might update an object not in the enclosing context's modifies clause
+opaqueBlock.dfy(224,2): Error: assertion might not hold
 
-Dafny program verifier finished with 3 verified, 14 errors
+Dafny program verifier finished with 3 verified, 16 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy
index 6014efe5df..f8819900f8 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy
@@ -1,6 +1,4 @@
-// UNSUPPORTED: macosx
-// Unsupported because the resource count is slightly different on macosx
-// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --allow-deprecation --performance-stats=1
+// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --allow-deprecation --performance-stats=100
 codatatype Stream<T> = Cons(head: T, tail: Stream)
 
 ghost function Upward(n: int): Stream<int>
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect
index 53fd056694..d8c1626435 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect
@@ -31,5 +31,5 @@ CoinductiveProofs.dfy(208,21): Related location: this is the postcondition that
 CoinductiveProofs.dfy(4,23): Related location: this proposition could not be proved
 
 Dafny program verifier finished with 23 verified, 12 errors
-Total resources used is 748143
-Max resources used by VC is 59297
+Total resources used is 748100
+Max resources used by VC is 59300