From b31f51bf479b0ae641f77e6f407b0dff2b2ec808 Mon Sep 17 00:00:00 2001
From: Yi Zhang <zorozy@gmail.com>
Date: Mon, 12 Aug 2019 23:33:05 -0500
Subject: [PATCH] rename G => GAAS in one of the lemmas. (#433)

---
 .../specs/ds-token-erc20/abstract-semantics-segmented-gas.k | 6 +++---
 tests/specs/hkg-erc20/abstract-semantics-segmented-gas.k    | 6 +++---
 tests/specs/hobby-erc20/abstract-semantics-segmented-gas.k  | 6 +++---
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/tests/specs/ds-token-erc20/abstract-semantics-segmented-gas.k b/tests/specs/ds-token-erc20/abstract-semantics-segmented-gas.k
index 1829bcf479..5a51123c11 100644
--- a/tests/specs/ds-token-erc20/abstract-semantics-segmented-gas.k
+++ b/tests/specs/ds-token-erc20/abstract-semantics-segmented-gas.k
@@ -15,10 +15,10 @@ module ABSTRACT-SEMANTICS-SEGMENTED-GAS
   // ########################
 
   // accumulate the gas cost and never run out of gas
-  rule <k> G ~> #deductGas => . ... </k>
-       <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM) </gas>
+  rule <k> GAAS:Int ~> #deductGas => . ... </k>
+       <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int GAAS, MEM) </gas>
        <callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
-    requires #notKLabel(G, "#symCmem")
+    requires #notKLabel(GAAS, "#symCmem")
     [trusted, matching(#gas)]
 
   rule <k> #symCmem(MEM') ~> #deductGas => . ... </k>
diff --git a/tests/specs/hkg-erc20/abstract-semantics-segmented-gas.k b/tests/specs/hkg-erc20/abstract-semantics-segmented-gas.k
index 1829bcf479..5a51123c11 100644
--- a/tests/specs/hkg-erc20/abstract-semantics-segmented-gas.k
+++ b/tests/specs/hkg-erc20/abstract-semantics-segmented-gas.k
@@ -15,10 +15,10 @@ module ABSTRACT-SEMANTICS-SEGMENTED-GAS
   // ########################
 
   // accumulate the gas cost and never run out of gas
-  rule <k> G ~> #deductGas => . ... </k>
-       <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM) </gas>
+  rule <k> GAAS:Int ~> #deductGas => . ... </k>
+       <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int GAAS, MEM) </gas>
        <callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
-    requires #notKLabel(G, "#symCmem")
+    requires #notKLabel(GAAS, "#symCmem")
     [trusted, matching(#gas)]
 
   rule <k> #symCmem(MEM') ~> #deductGas => . ... </k>
diff --git a/tests/specs/hobby-erc20/abstract-semantics-segmented-gas.k b/tests/specs/hobby-erc20/abstract-semantics-segmented-gas.k
index 1829bcf479..5a51123c11 100644
--- a/tests/specs/hobby-erc20/abstract-semantics-segmented-gas.k
+++ b/tests/specs/hobby-erc20/abstract-semantics-segmented-gas.k
@@ -15,10 +15,10 @@ module ABSTRACT-SEMANTICS-SEGMENTED-GAS
   // ########################
 
   // accumulate the gas cost and never run out of gas
-  rule <k> G ~> #deductGas => . ... </k>
-       <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM) </gas>
+  rule <k> GAAS:Int ~> #deductGas => . ... </k>
+       <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int GAAS, MEM) </gas>
        <callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
-    requires #notKLabel(G, "#symCmem")
+    requires #notKLabel(GAAS, "#symCmem")
     [trusted, matching(#gas)]
 
   rule <k> #symCmem(MEM') ~> #deductGas => . ... </k>