updated comment on ci example

nyu-acsys · Oct 29, 2024 · 36a2f6c · 36a2f6c
1 parent 3ebfd50
commit 36a2f6c
Showing 1 changed file with 4 additions and 7 deletions.
diff --git a/test/ci/back-end/witness_comp.rav b/test/ci/back-end/witness_comp.rav
@@ -10,11 +10,8 @@ proc p() {
     exhale exists v: Int :: own(x, c, v, 1.0) && pred1(x, v);
 
     // After witness computation, the above exhale gets replaced by:
-    //     exhale own(x, c, c$Heap[x].frac_proj1, 1.0) && pred1(x, c$Heap[x].frac_proj1);
-
-    // which gets translated to:
-    //     exhale own(x, c, c$Heap[x].frac_proj1, 1.0) 
-    //     exhale pred1(x, c$Heap[x].frac_proj1);
-
-    // After the first exhale, the value `c$Heap[x].frac_proj1` is no longer available.
+    //     assume $skolem_expr_placeholder$v = c$Heap[x].frac_proj1;
+    //     exhale
+    //        own(x, c, $skolem_expr_placeholder$v, 1.0) && 
+    //        pred1(x, $skolem_expr_placeholder$v);
 }