Merge remote-tracking branch 'origin/master' into release

deps/k_release

@@ -1 +1 @@
-7.1.131
+7.1.132

flake.nix

@@ -2,7 +2,7 @@
   description = "A flake for the KEVM Semantics";
 
   inputs = {
-    k-framework.url = "github:runtimeverification/k/v7.1.131";
+    k-framework.url = "github:runtimeverification/k/v7.1.132";
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";
     rv-utils.follows = "k-framework/rv-utils";

kevm-pyk/pyproject.toml

@@ -13,7 +13,7 @@ authors = [
 [tool.poetry.dependencies]
 python = "^3.10"
 pathos = "*"
-kframework = "7.1.131"
+kframework = "7.1.132"
 tomlkit = "^0.11.6"
 
 [tool.poetry.group.dev.dependencies]

tests/specs/examples/sum-to-n-foundry-spec.k

@@ -41,7 +41,7 @@ claim [foundry-sum-to-n-loop-invariant]:
             #computeValidJumpDests(b"`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x01,W`\x005`\xe0\x1c\x80c]\xe2/\x07\x11a\x00\xadW\x80c\xa1\x18\xe1\x02\x11a\x00qW\x80c\xa1\x18\xe1\x02\x14a\x02bW\x80c\xbaAO\xa6\x14a\x02uW\x80c\xd3\x13\x94\r\x14a\x02\x8dW\x80c\xf8\xcc\xbfG\x14a\x02\xa0W\x80c\xfav&\xd4\x14a\x02\xb3W`\x00\x80\xfd[\x80c]\xe2/\x07\x14a\x02\x03W\x80cm]9\xdf\x14a\x02\x16W\x80c~\x8e#\xd0\x14a\x02)W\x80c\x88~O\xdb\x14a\x02<W\x80c\x8f\xe3J\xed\x14a\x02OW`\x00\x80\xfd[\x80c:v\x84c\x11a\x00\xf4W\x80c:v\x84c\x14a\x01\x9aW\x80c@\xcaq\x1a\x14a\x01\xcdW\x80cN\x94\xceW\x14a\x01\xd5W\x80cQ\xcd\xc1\x92\x14a\x01\xe8W\x80cZ\x98\xa5\xc0\x14a\x01\xfbW`\x00\x80\xfd[\x80c\x06\xac\x150\x14a\x011W\x80c\rG(y\x14a\x01FW\x80c\r\xe4\xeb\x16\x14a\x01aW\x80c\x18\x1f\x88\xec\x14a\x01tW\x80c0Gn'\x14a\x01\x87W[`\x00\x80\xfd[a\x01Da\x01?6`\x04a\x11\xd2V[a\x02\xc0V[\x00[a\x01Na\x03\x19V[`@Q\x90\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[a\x01Da\x01o6`\x04a\x11\xf4V[a\x03+V[a\x01Da\x01\x826`\x04a\x11\xf4V[a\x03\x89V[a\x01Da\x01\x956`\x04a\x11\xf4V[a\x03\xa6V[a\x01\xb5sq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01a\x01XV[a\x01Na\x04\nV[a\x01Da\x01\xe36`\x04a\x11\xf4V[a\x04\x16V[a\x01Da\x01\xf66`\x04a\x12#V[a\x04\xbcV[a\x01Na\x05\x1cV[a\x01Da\x02\x116`\x04a\x12#V[a\x05(V[a\x01Da\x02$6`\x04a\x11\xd2V[a\x05~V[a\x01Na\x0276`\x04a\x11\xf4V[a\x05\x89V[a\x01Da\x02J6`\x04a\x11\xf4V[a\x06'V[a\x01Da\x02]6`\x04a\x12#V[a\x06\xc1V[a\x01Da\x02p6`\x04a\x11\xd2V[a\x07;V[a\x02}a\x07\xa5V[`@Q\x90\x15\x15\x81R` \x01a\x01XV[a\x01Da\x02\x9b6`\x04a\x12#V[a\x08\xd0V[`\x00Ta\x02}\x90b\x01\x00\x00\x90\x04`\xff\x16\x81V[`\x00Ta\x02}\x90`\xff\x16\x81V[`\x00a\x02\xcb\x83a\tJV[\x90Pa\x02\xe2\x81\x15\x80a\x02\xddWP`\x01\x84\x11[a\t\x9bV[a\x03\x14`\x02\x83\x10\x80a\x02\xf4WP\x83\x83\x10\x15[\x80a\x02\xfdWP\x81\x15[\x80a\x02\xddWPa\x03\r\x83\x85a\x12\xf7V[\x15\x15a\t\x9bV[PPPV[`\x00a\x03&a\x03\xe8a\x05\x89V[\x90P\x90V[`\x00a\x036\x82a\n\x0fV[\x90P`\x00a\x03D\x82\x83a\nWV[\x90P`\x00\x83\x82\x11\x15a\x03aWa\x03Z\x84\x83a\x13!V[\x90Pa\x03nV[a\x03k\x83\x83a\x13!V[\x90P[a\x03\x83a\x03|`d\x86a\x138V[\x82\x10a\t\x9bV[PPPPV[a\x03\xa3a\x03\x95\x82a\tJV[a\x03\x9e\x83a\n\x92V[a\n\xe3V[PV[`\x00a\x03\xb1\x82a\tJV[\x90P\x80\x80a\x03\xbfWP`\x02\x82\x10[\x15a\x03\xc8WPPV[`\x02[\x82\x81\x10\x15a\x03\xfbWa\x03\xdd\x81\x84a\x12\xf7V[`\x00\x03a\x03\xe9WPPPV[\x80a\x03\xf3\x81a\x13LV[\x91PPa\x03\xcbV[Pa\x04\x06`\x00a\t\x9bV[PPV[`\x00a\x03&`\na\x05\x89V[`@Qc&1\xf2\xb1`\xe1\x1b\x81R`d\x82\x11\x15`\x04\x82\x01Rsq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-\x90cLc\xe5b\x90`$\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x04fW`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x04zW=`\x00\x80>=`\x00\xfd[PPPP`\x00`\x02\x82`\x01a\x04\x8f\x91\x90a\x13eV[a\x04\x99\x90\x84a\x13}V[a\x04\xa3\x91\x90a\x138V[\x90P`\x00a\x04\xb0\x83a\f`V[\x90Pa\x03\x14\x82\x82a\f\x92V[`\x00a\x04\xc7\x82a\rqV[\x90P`\x01`\x00[\x83Q\x81\x10\x80\x15a\x04\xdbWP\x81[\x15a\x05\x12W\x83\x81\x81Q\x81\x10a\x04\xf2Wa\x04\xf2a\x13\x9cV[` \x02` \x01\x01Q\x83\x10\x15\x91P\x80\x80a\x05\n\x90a\x13LV[\x91PPa\x04\xceV[Pa\x03\x14\x81a\t\x9bV[`\x00a\x03&`da\x05\x89V[`\x00a\x053\x82a\r\xd0V[\x90P`\x01`\x00[\x83Q\x81\x10\x80\x15a\x05GWP\x81[\x15a\x05\x12W\x83\x81\x81Q\x81\x10a\x05^Wa\x05^a\x13\x9cV[` \x02` \x01\x01Q\x83\x10\x15\x91P\x80\x80a\x05v\x90a\x13LV[\x91PPa\x05:V[`\x00a\x02\xcb\x83a\x0e.V[`@Qc&1\xf2\xb1`\xe1\x1b\x81Rf\xb8\x17\x02\xe0\\\x0bo\x82\x11\x15`\x04\x82\x01R`\x00\x90sq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-\x90cLc\xe5b\x90`$\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x05\xe2W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x05\xf6W=`\x00\x80>=`\x00\xfd[PPPP`\x00[\x82\x15a\x06!Wa\x06\r\x83\x82a\x13eV[\x90Pa\x06\x1a`\x01\x84a\x13!V[\x92Pa\x05\xfdV[\x92\x91PPV[`@Qc&1\xf2\xb1`\xe1\x1b\x81R`d\x82\x11\x15`\x04\x82\x01Rsq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-\x90cLc\xe5b\x90`$\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x06wW`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x06\x8bW=`\x00\x80>=`\x00\xfd[PPPP`\x00`\x02\x82`\x01a\x06\xa0\x91\x90a\x13eV[a\x06\xaa\x90\x84a\x13}V[a\x06\xb4\x91\x90a\x138V[\x90P`\x00a\x04\xb0\x83a\x0eeV[`\x00a\x06\xcc\x82a\x0e\x8fV[\x90P`\x01\x80[\x82Q\x81\x10\x80\x15a\x06\xdfWP\x81[\x15a\x05\x12W\x83\x81\x81Q\x81\x10a\x06\xf6Wa\x06\xf6a\x13\x9cV[` \x02` \x01\x01Q\x84`\x01\x83a\x07\f\x91\x90a\x13!V[\x81Q\x81\x10a\x07\x1cWa\x07\x1ca\x13\x9cV[` \x02` \x01\x01Q\x11\x15\x91P\x80\x80a\x073\x90a\x13LV[\x91PPa\x06\xd2V[`\x00a\x07F\x83a\x0e\xbbV[\x90P\x82`\x00\x03a\x07[Wa\x03\x14\x81`\x00a\f\x92V[a\x07ga\x02\xdd\x82a\tJV[`\x00a\x07|a\x07w`\x01\x86a\x13!V[a\x0e\xbbV[\x90Pa\x03\x83\x81\x84\x11\x15\x80a\x07\x90WP\x82\x84\x10\x15[\x80a\x02\xddWPa\x07\x9f\x84a\tJV[\x15a\t\x9bV[`\x00\x80Ta\x01\x00\x90\x04`\xff\x16\x15a\x07\xc5WP`\x00Ta\x01\x00\x90\x04`\xff\x16\x90V[`\x00sq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-;\x15a\x08\xcbW`@\x80Qsq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-` \x82\x01\x81\x90Re\x19\x98Z[\x19Y`\xd2\x1b\x82\x84\x01R\x82Q\x80\x83\x03\x84\x01\x81R``\x83\x01\x90\x93R`\x00\x92\x90\x91a\x08S\x91\x7ff\x7f\x9dp\xcaA\x1dp\xea\xd5\r\x8d\\\"\x07\r\xaf\xc3j\xd7_=\xcf^r7\xb2*\xde\x9a\xec\xc4\x91`\x80\x01a\x13\xdeV[`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\x08m\x91a\x14\x0fV[`\x00`@Q\x80\x83\x03\x81`\x00\x86Z\xf1\x91PP=\x80`\x00\x81\x14a\x08\xaaW`@Q\x91P`\x1f\x19`?=\x01\x16\x82\x01`@R=\x82R=`\x00` \x84\x01>a\x08\xafV[``\x91P[P\x91PP\x80\x80` \x01\x90Q\x81\x01\x90a\x08\xc7\x91\x90a\x14+V[\x91PP[\x91\x90PV[`\x00a\x08\xdb\x82a\x0e\xf5V[\x90P`\x01\x80[\x82Q\x81\x10\x80\x15a\x08\xeeWP\x81[\x15a\x05\x12W\x83\x81\x81Q\x81\x10a\t\x05Wa\t\x05a\x13\x9cV[` \x02` \x01\x01Q\x84`\x01\x83a\t\x1b\x91\x90a\x13!V[\x81Q\x81\x10a\t+Wa\t+a\x13\x9cV[` \x02` \x01\x01Q\x11\x15\x91P\x80\x80a\tB\x90a\x13LV[\x91PPa\x08\xe1V[`\x00`\x02\x82\x10\x15a\t]WP`\x00\x91\x90PV[`\x02[\x82\x81\x10\x15a\t\x92Wa\tr\x81\x84a\x12\xf7V[\x15a\t\x80WP`\x00\x92\x91PPV[\x80a\t\x8a\x81a\x13LV[\x91PPa\t`V[P`\x01\x92\x91PPV[\x80a\x03\xa3W\x7fA0O\xac\xd92=u\xb1\x1b\xcd\xd6\t\xcb8\xef\xff\xfd\xb0W\x10\xf7\xca\xf0\xe9\xb1lm\x9dp\x9fP`@Qa\t\xff\x90` \x80\x82R`\x17\x90\x82\x01R\x7fError: Assertion Failed\x00\x00\x00\x00\x00\x00\x00\x00\x00`@\x82\x01R``\x01\x90V[`@Q\x80\x91\x03\x90\xa1a\x03\xa3a\x0f\x17V[`\x00\x81`\x00\x03a\n!WP`\x00\x91\x90PV[\x81[\x80\x91P`\x02\x81a\n3\x85\x84a\x10#V[a\n=\x91\x90a\x13eV[a\nG\x91\x90a\x138V[\x90P\x81\x81\x03a\n#W[P\x91\x90PV[`\x00g\r\xe0\xb6\xb3\xa7d\x00\x00a\nm`\x02\x82a\x138V[a\nw\x84\x86a\x13}V[a\n\x81\x91\x90a\x13eV[a\n\x8b\x91\x90a\x138V[\x93\x92PPPV[`\x00`\x02\x82\x10\x15a\n\xa5WP`\x00\x91\x90PV[`\x02[a\n\xb3`\x02\x84a\x138V[\x81\x11a\t\x92Wa\n\xc3\x81\x84a\x12\xf7V[\x15a\n\xd1WP`\x00\x92\x91PPV[\x80a\n\xdb\x81a\x13LV[\x91PPa\n\xa8V[\x80\x15\x15\x82\x15\x15\x14a\x04\x06W\x7fA0O\xac\xd92=u\xb1\x1b\xcd\xd6\t\xcb8\xef\xff\xfd\xb0W\x10\xf7\xca\xf0\xe9\xb1lm\x9dp\x9fP`@Qa\x0bX\x90` \x80\x82R`\"\x90\x82\x01R\x7fError: a == b not satisfied [boo`@\x82\x01Ral]`\xf0\x1b``\x82\x01R`\x80\x01\x90V[`@Q\x80\x91\x03\x90\xa1\x7f(\x0fDF\xb2\x8a\x13rA}\xdae\x8d0\xb9[)\x92\xb1*\xc9\xc7\xf3xS_)\xa9z\xcf5\x83\x81a\x0b\xa9W`@Q\x80`@\x01`@R\x80`\x05\x81R` \x01dfalse`\xd8\x1b\x81RPa\x0b\xc7V[`@Q\x80`@\x01`@R\x80`\x04\x81R` \x01ctrue`\xe0\x1b\x81RP[`@Qa\x0b\xd4\x91\x90a\x14yV[`@Q\x80\x91\x03\x90\xa1\x7f(\x0fDF\xb2\x8a\x13rA}\xdae\x8d0\xb9[)\x92\xb1*\xc9\xc7\xf3xS_)\xa9z\xcf5\x83\x82a\f%W`@Q\x80`@\x01`@R\x80`\x05\x81R` \x01dfalse`\xd8\x1b\x81RPa\fCV[`@Q\x80`@\x01`@R\x80`\x04\x81R` \x01ctrue`\xe0\x1b\x81RP[`@Qa\fP\x91\x90a\x14\xbdV[`@Q\x80\x91\x03\x90\xa1a\x04\x06a\x0f\x17V[`\x00\x80\x80[\x83\x81\x10\x15a\f\x8bWa\fw\x81\x83a\x13eV[\x91P\x80a\f\x83\x81a\x13LV[\x91PPa\feV[P\x92\x91PPV[\x80\x82\x14a\x04\x06W\x7fA0O\xac\xd92=u\xb1\x1b\xcd\xd6\t\xcb8\xef\xff\xfd\xb0W\x10\xf7\xca\xf0\xe9\xb1lm\x9dp\x9fP`@Qa\r\x03\x90` \x80\x82R`\"\x90\x82\x01R\x7fError: a == b not satisfied [uin`@\x82\x01Rat]`\xf0\x1b``\x82\x01R`\x80\x01\x90V[`@Q\x80\x91\x03\x90\xa1\x7f\xb2\xde/\xbe\x80\x1a\r\xf6\xc0\xcb\xdd\xfdD\x8b\xa3\xc4\x1dH\xa0@\xca5\xc5l\x81\x96\xef\x0f\xca\xe7!\xa8\x81`@Qa\r:\x91\x90a\x14\xe7V[`@Q\x80\x91\x03\x90\xa1\x7f\xb2\xde/\xbe\x80\x1a\r\xf6\xc0\xcb\xdd\xfdD\x8b\xa3\xc4\x1dH\xa0@\xca5\xc5l\x81\x96\xef\x0f\xca\xe7!\xa8\x82`@Qa\fP\x91\x90a\x15\x1fV[`\x00\x80`\x01[\x83Q\x81\x10\x15a\f\x8bW\x81\x84\x82\x81Q\x81\x10a\r\x93Wa\r\x93a\x13\x9cV[` \x02` \x01\x01Q\x11\x15a\r\xbeW\x83\x81\x81Q\x81\x10a\r\xb3Wa\r\xb3a\x13\x9cV[` \x02` \x01\x01Q\x91P[\x80a\r\xc8\x81a\x13LV[\x91PPa\rwV[`\x00\x80\x80[\x83Q\x81\x10\x15a\f\x8bW\x81\x84\x82\x81Q\x81\x10a\r\xf1Wa\r\xf1a\x13\x9cV[` \x02` \x01\x01Q\x11\x15a\x0e\x1cW\x83\x81\x81Q\x81\x10a\x0e\x11Wa\x0e\x11a\x13\x9cV[` \x02` \x01\x01Q\x91P[\x80a\x0e&\x81a\x13LV[\x91PPa\r\xd5V[`\x00`\x02[\x82\x81\x10\x15a\t\x92Wa\x0eE\x81\x84a\x12\xf7V[\x15a\x0eSWP`\x00\x92\x91PPV[\x80a\x0e]\x81a\x13LV[\x91PPa\x0e3V[`\x00\x80\x80[\x83\x81\x11a\f\x8bWa\x0e{\x81\x83a\x13eV[\x91P\x80a\x0e\x87\x81a\x13LV[\x91PPa\x0ejV[```\x01\x82Q\x11a\x0e\x9eWP\x90V[a\x0e\xb7\x82`\x00`\x01\x85Qa\x0e\xb2\x91\x90a\x13!V[a\x10CV[P\x90V[`\x00\x80[\x82\x81\x10\x15a\nQW\x81a\x0e\xd1\x81a\x13LV[\x92PPa\x0e\xdd\x82a\tJV[\x15a\x0e\xf0W\x80a\x0e\xec\x81a\x13LV[\x91PP[a\x0e\xbfV[```\x01\x82Q\x11a\x0f\x04WP\x90V[a\x0e\xb7\x82`\x01\x80\x85Qa\x0e\xb2\x91\x90a\x13!V[sq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-;\x15a\x10\x12W`@\x80Qsq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-` \x82\x01\x81\x90Re\x19\x98Z[\x19Y`\xd2\x1b\x92\x82\x01\x92\x90\x92R`\x01``\x82\x01R`\x00\x91\x90\x7fp\xca\x10\xbb\xd0\xdb\xfd\x90 \xa9\xf4\xb14\x02\xc1l\xb1 p^\r\x1c\n\xea\xb1\x0f\xa3S\xaeXo\xc4\x90`\x80\x01`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\x0f\xb1\x92\x91` \x01a\x13\xdeV[`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\x0f\xcb\x91a\x14\x0fV[`\x00`@Q\x80\x83\x03\x81`\x00\x86Z\xf1\x91PP=\x80`\x00\x81\x14a\x10\x08W`@Q\x91P`\x1f\x19`?=\x01\x16\x82\x01`@R=\x82R=`\x00` \x84\x01>a\x10\rV[``\x91P[PPPP[`\x00\x80Ta\xff\x00\x19\x16a\x01\x00\x17\x90UV[`\x00\x81a\x101`\x02\x82a\x138V[a\nwg\r\xe0\xb6\xb3\xa7d\x00\x00\x86a\x13}V[\x80\x82\x10a\x10OWPPPV[\x81\x81`\x00\x85`\x02a\x10`\x85\x85a\x13!V[a\x10j\x91\x90a\x138V[a\x10t\x90\x87a\x13eV[\x81Q\x81\x10a\x10\x84Wa\x10\x84a\x13\x9cV[` \x02` \x01\x01Q\x90P[\x81\x83\x11a\x11\xa4W[\x80\x86\x84\x81Q\x81\x10a\x10\xaaWa\x10\xaaa\x13\x9cV[` \x02` \x01\x01Q\x10\x15a\x10\xcaW\x82a\x10\xc2\x81a\x13LV[\x93PPa\x10\x97V[\x85\x82\x81Q\x81\x10a\x10\xdcWa\x10\xdca\x13\x9cV[` \x02` \x01\x01Q\x81\x10\x80\x15a\x10\xf2WP`\x00\x82\x11[\x15a\x11\tW\x81a\x11\x01\x81a\x15IV[\x92PPa\x10\xcaV[\x81\x83\x11a\x11\x9fW\x85\x82\x81Q\x81\x10a\x11\"Wa\x11\"a\x13\x9cV[` \x02` \x01\x01Q\x86\x84\x81Q\x81\x10a\x11<Wa\x11<a\x13\x9cV[` \x02` \x01\x01Q\x87\x85\x81Q\x81\x10a\x11VWa\x11Va\x13\x9cV[` \x02` \x01\x01\x88\x85\x81Q\x81\x10a\x11oWa\x11oa\x13\x9cV[` \x90\x81\x02\x91\x90\x91\x01\x01\x91\x90\x91RR\x82a\x11\x88\x81a\x13LV[\x93PP\x81\x15a\x11\x9fW\x81a\x11\x9b\x81a\x15IV[\x92PP[a\x10\x8fV[\x81\x85\x10\x15a\x11\xb7Wa\x11\xb7\x86\x86\x84a\x10CV[\x83\x83\x10\x15a\x11\xcaWa\x11\xca\x86\x84\x86a\x10CV[PPPPPPV[`\x00\x80`@\x83\x85\x03\x12\x15a\x11\xe5W`\x00\x80\xfd[PP\x805\x92` \x90\x91\x015\x91PV[`\x00` \x82\x84\x03\x12\x15a\x12\x06W`\x00\x80\xfd[P5\x91\x90PV[cNH{q`\xe0\x1b`\x00R`A`\x04R`$`\x00\xfd[`\x00` \x80\x83\x85\x03\x12\x15a\x126W`\x00\x80\xfd[\x825g\xff\xff\xff\xff\xff\xff\xff\xff\x80\x82\x11\x15a\x12NW`\x00\x80\xfd[\x81\x85\x01\x91P\x85`\x1f\x83\x01\x12a\x12bW`\x00\x80\xfd[\x815\x81\x81\x11\x15a\x12tWa\x12ta\x12\rV[\x80`\x05\x1b`@Q`\x1f\x19`?\x83\x01\x16\x81\x01\x81\x81\x10\x85\x82\x11\x17\x15a\x12\x99Wa\x12\x99a\x12\rV[`@R\x91\x82R\x84\x82\x01\x92P\x83\x81\x01\x85\x01\x91\x88\x83\x11\x15a\x12\xb7W`\x00\x80\xfd[\x93\x85\x01\x93[\x82\x85\x10\x15a\x12\xd5W\x845\x84R\x93\x85\x01\x93\x92\x85\x01\x92a\x12\xbcV[\x98\x97PPPPPPPPV[cNH{q`\xe0\x1b`\x00R`\x12`\x04R`$`\x00\xfd[`\x00\x82a\x13\x06Wa\x13\x06a\x12\xe1V[P\x06\x90V[cNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[`\x00\x82\x82\x10\x15a\x133Wa\x133a\x13\x0bV[P\x03\x90V[`\x00\x82a\x13GWa\x13Ga\x12\xe1V[P\x04\x90V[`\x00`\x01\x82\x01a\x13^Wa\x13^a\x13\x0bV[P`\x01\x01\x90V[`\x00\x82\x19\x82\x11\x15a\x13xWa\x13xa\x13\x0bV[P\x01\x90V[`\x00\x81`\x00\x19\x04\x83\x11\x82\x15\x15\x16\x15a\x13\x97Wa\x13\x97a\x13\x0bV[P\x02\x90V[cNH{q`\xe0\x1b`\x00R`2`\x04R`$`\x00\xfd[`\x00[\x83\x81\x10\x15a\x13\xcdW\x81\x81\x01Q\x83\x82\x01R` \x01a\x13\xb5V[\x83\x81\x11\x15a\x03\x83WPP`\x00\x91\x01RV[`\x01`\x01`\xe0\x1b\x03\x19\x83\x16\x81R\x81Q`\x00\x90a\x14\x01\x81`\x04\x85\x01` \x87\x01a\x13\xb2V[\x91\x90\x91\x01`\x04\x01\x93\x92PPPV[`\x00\x82Qa\x14!\x81\x84` \x87\x01a\x13\xb2V[\x91\x90\x91\x01\x92\x91PPV[`\x00` \x82\x84\x03\x12\x15a\x14=W`\x00\x80\xfd[\x81Q\x80\x15\x15\x81\x14a\n\x8bW`\x00\x80\xfd[`\x00\x81Q\x80\x84Ra\x14e\x81` \x86\x01` \x86\x01a\x13\xb2V[`\x1f\x01`\x1f\x19\x16\x92\x90\x92\x01` \x01\x92\x91PPV[`@\x81R`\x00a\x14\xa3`@\x83\x01`\n\x81Ri\x08\x08\x11^\x1c\x19X\xdd\x19Y`\xb2\x1b` \x82\x01R`@\x01\x90V[\x82\x81\x03` \x84\x01Ra\x14\xb5\x81\x85a\x14MV[\x94\x93PPPPV[`@\x81R`\x00a\x14\xa3`@\x83\x01`\n\x81Ri\x08\x08\x08\x08\x10X\xdd\x1dX[`\xb2\x1b` \x82\x01R`@\x01\x90V[`@\x81R`\x00a\x15\x11`@\x83\x01`\n\x81Ri\x08\x08\x11^\x1c\x19X\xdd\x19Y`\xb2\x1b` \x82\x01R`@\x01\x90V[\x90P\x82` \x83\x01R\x92\x91PPV[`@\x81R`\x00a\x15\x11`@\x83\x01`\n\x81Ri\x08\x08\x08\x08\x10X\xdd\x1dX[`\xb2\x1b` \x82\x01R`@\x01\x90V[`\x00\x81a\x15XWa\x15Xa\x13\x0bV[P`\x00\x19\x01\x90V\xfe\xa2dipfsX\"\x12 \xea\xd1\xd9I\x07y\x90\x0b\xd7\rna\x8b\x84\xe5\xcbKp\x08\xf5\xbf\x9a\xc3\xa1'\x1c\xf2\x89\xdd\xc2\x1f\x07dsolcC\x00\x08\r\x003")
           </jumpDests>
           <wordStack>
-              (S => (S +Int ((N *Int (N +Int 1)) /Int 2)))
+              (S => (S +Int ((N *Int (N +Int 1)) divInt 2)))
             : 0
             : (N => 0)
             : 334
@@ -64,7 +64,7 @@ claim [foundry-sum-to-n-loop-invariant]:
   </kevm>
 
   requires 0 <Int N
-   andBool #rangeUInt(256, S +Int ((N *Int (N +Int 1)) /Int 2))
+   andBool #rangeUInt(256, S +Int ((N *Int (N +Int 1)) divInt 2))
    andBool #rangeUInt(256, N)
    andBool #rangeUInt(256, S)
    andBool GAS_AMT >=Int N *Int 178