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>