From 2790eff1526343b0fa345547ecb3a0aeff8ccd46 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 27 Mar 2024 18:07:01 -0500 Subject: [PATCH] fix another spec --- tests/specs/functional/infinite-gas-spec.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/specs/functional/infinite-gas-spec.k b/tests/specs/functional/infinite-gas-spec.k index c04916fbaf..6477557489 100644 --- 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]: runLemma(#allBut64th(#gas(_G)) doneLemma(false) ... - claim [gas.comp.19]: runLemma(Gverylow < _ > <=Gas #gas(_)) => doneLemma(true) ... + claim [gas.comp.19]: runLemma(Gverylow( _ ) <=Gas #gas(_)) => doneLemma(true) ... claim [gas.comp.20]: runLemma(Gexp(SCHED) +Int Gexpbyte(SCHED) *Int ( log2Int ( W1 ) /Int 8 +Int 1 ) <=Gas #gas(_)) => doneLemma(true) ... requires 0 runLemma(#gas(_) doneLemma(false) ... requires 0