recompiling hkg standard token and runing proof produce different result

[huangyg11]

I would like to proof a simple erc20 token, and get error:

[Error] Critical: Z3 crashed on input query:
(declare-sort InternalOp)
(declare-sort K)
(declare-sort WordStack)
(declare-fun sizeWordStackAux (WordStack Int) Int)
(declare-fun sizeWordStack (WordStack) Int)
(declare-fun smt_keccak (WordStack) Int)
(declare-fun asByteStack (Int WordStack) WordStack)
(declare-fun chop (Int) Int)
(declare-fun smt_nthbyteof (Int Int Int) Int)
(declare-fun asWord (WordStack) Int)
(assert (forall ((|_784| Int)) (= (chop |_784|) (mod |_784|
115792089237316195423570985008687907853269984665640564039457584007913129639936))))
(assert (forall ((|_490| WordStack)(|_491| Int)) (= (>= (sizeWordStackAux
|_490| |_491|) 0) true)))
(declare-fun |_1215| () Int)
(declare-fun |R__432| () K)
(declare-fun |_1170| () Int)
(declare-fun |_1172| () Int)
(declare-fun |_1171| () Int)
(declare-fun |_3920| () K)
(declare-fun |_3922| () K)
(declare-fun |_3921| () InternalOp)
(assert (and (= (<= 0 |_1171|) true) (= (<= 0 |_1170|) true) (= (<= 0 |_1172|)
true) (= _3920 _3921) (= (< |_1172|
1461501637330902918203684832716283019655932542976) true) (= (<= 0 |_1215|)
true) (= (< |_1170| 1461501637330902918203684832716283019655932542976) true) (=
_3922 (smt_seq_elem |R__432|)) (= (< |_1215|
1461501637330902918203684832716283019655932542976) true) (= (< |_1171| 1024)
true)))
result:
(error "line 21 column 99: Sorts K and InternalOp are incompatible")
[Warning] Critical: missing SMTLib translation for Map:lookup (missing SMTLib
translation for Map:lookup)
[Warning] Critical: missing SMTLib translation for in_keys()_MAP (missing
SMTLib translation for in_keys()_MAP)

So I try to compile the sample.
I recompile the hkg standard token ( standardtoken.inlined.sol ) using remix (v0.4.19), the copy the bytes to hkg-erc20-spec.ini, and run
python3 resources/gen-spec.py erc20/module-tmpl.k erc20/spec-tmpl.k erc20/hkg/hkg-erc20-spec.ini totalSupply totalSupply > specs/hkg-erc20/totalSupply-spec.k

and run proof:
./kevm prove tests/proofs/specs/hkg-erc20/totalSupply-spec.k.

it output true originly, but this time it output somthing different( attached in the last). I am not sure if something goes wrong.

tmp.txt