From c7aa17b4fe8272e3da4da981a8803db7e20321ce Mon Sep 17 00:00:00 2001
From: septract <miked@galois.com>
Date: Fri, 19 Jul 2024 20:46:00 -0700
Subject: [PATCH] Remove redundant instantiate, add stronger post to write_5
 example

---
 .../dafny-tutorial/working/linear_search.c               | 1 -
 src/example-archive/simple-examples/working/write_5.c    | 9 +++++++--
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/example-archive/dafny-tutorial/working/linear_search.c b/src/example-archive/dafny-tutorial/working/linear_search.c
index 8d9b0781..17b42980 100644
--- a/src/example-archive/dafny-tutorial/working/linear_search.c
+++ b/src/example-archive/dafny-tutorial/working/linear_search.c
@@ -26,7 +26,6 @@ int linear_search(int *a, int length, int key)
         each (i32 j; 0i32 <= j && j < idx) {IndexPre[j] != key}; @*/
   {
     /*@ extract Owned<int>, idx; @*/
-    /*@ instantiate good<int>, idx;  @*/
     if (*(a + idx) == key)
     {
       return idx;
diff --git a/src/example-archive/simple-examples/working/write_5.c b/src/example-archive/simple-examples/working/write_5.c
index 6beede19..2fe0c727 100644
--- a/src/example-archive/simple-examples/working/write_5.c
+++ b/src/example-archive/simple-examples/working/write_5.c
@@ -6,7 +6,9 @@ void write_5(int *pair)
       take Cell2Pre = Owned(pair + 1i32); @*/
 /*@ ensures 
       take Cell1Post = Owned(pair);
-      take Cell2Post = Owned(pair + 1i32); @*/
+      take Cell2Post = Owned(pair + 1i32); 
+      Cell1Post == 7i32; 
+      Cell2Post == 8i32; @*/
 {
   pair[0] = 7;
   pair[1] = 8;
@@ -18,7 +20,10 @@ void write_5_alt(int *pair)
 /*@ requires 
       take PairPre = each (i32 j; j == 0i32 || j == 1i32) {Owned(pair + j)}; @*/
 /*@ ensures 
-      take PairPost = each (i32 j; j == 0i32 || j == 1i32) {Owned(pair + j)}; @*/
+      take PairPost = each (i32 j; j == 0i32 || j == 1i32) {Owned(pair + j)}; 
+      PairPost[0i32] == 7i32; 
+      PairPost[1i32] == 8i32; 
+      @*/
 {
   /*@ extract Owned<int>, 0i32; @*/
   pair[0] = 7;