fix another spec

runtimeverification · Mar 27, 2024 · 2790eff · 2790eff
1 parent 0a386d1
commit 2790eff
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/tests/specs/functional/infinite-gas-spec.k b/tests/specs/functional/infinite-gas-spec.k
@@ -110,7 +110,7 @@ module INFINITE-GAS-SPEC
 
     claim [gas.comp.18]: <k> runLemma(#allBut64th(#gas(_G)) <Gas #gas(_G')) => doneLemma(false) ... </k>
 
-    claim [gas.comp.19]: <k> runLemma(Gverylow < _ > <=Gas #gas(_)) => doneLemma(true) ... </k>
+    claim [gas.comp.19]: <k> runLemma(Gverylow( _ ) <=Gas #gas(_)) => doneLemma(true) ... </k>
 
     claim [gas.comp.20]: <k> runLemma(Gexp(SCHED) +Int Gexpbyte(SCHED) *Int ( log2Int ( W1 ) /Int 8 +Int 1 ) <=Gas #gas(_)) => doneLemma(true)  ... </k> requires 0 <Int W1 andBool W1 <Int pow256
     claim [gas.comp.21]: <k> runLemma(#gas(_) <Gas Gexp(SCHED) +Int Gexpbyte(SCHED) *Int ( log2Int ( W1 ) /Int 8 +Int 1 ))  => doneLemma(false) ... </k> requires 0 <Int W1 andBool W1 <Int pow256