2 files changed, 5 insertions, 5 deletions
diff --git a/Test/dafny2/MonotonicHeapstate.dfy b/Test/dafny2/MonotonicHeapstate.dfy
index d6817ce9..b0032b44 100644
--- a/Test/dafny2/MonotonicHeapstate.dfy
+++ b/Test/dafny2/MonotonicHeapstate.dfy
@@ -12,7 +12,7 @@ module M0 {
 
     ghost var Repr: set<object>;
 
-    predicate Valid()
+    protected predicate Valid()
       reads this, Repr;
     {
       this in Repr && null !in Repr &&
@@ -58,7 +58,7 @@ module M1 refines M0 {
   class Expr {
     ghost var resolved: bool;
 
-    predicate Valid()
+    protected predicate Valid()
     {
       resolved ==>
         (kind == Binary ==> left.resolved && right.resolved)
@@ -104,7 +104,7 @@ module M2 refines M1 {
   class Expr {
     var decl: VarDecl;  // if kind==Ident, filled in during resolution
 
-    predicate Valid()
+    protected predicate Valid()
     {
       resolved ==>
         (kind == Ident ==> decl != null)
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index e39913a8..5314b6fa 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -5,7 +5,7 @@ abstract module A {
   import L = Library
   class {:autocontracts} StoreAndRetrieve<Thing(==)> {
     ghost var Contents: set<Thing>;
-    predicate Valid()
+    protected predicate Valid()
     {
       true
     }
@@ -31,7 +31,7 @@ abstract module A {
 module B refines A {
   class StoreAndRetrieve<Thing(==)> {
     var arr: seq<Thing>;
-    predicate Valid()
+    protected predicate Valid()
     {
       Contents == set x | x in arr
     }