Abnormal execution time of the SMTChecker about solidity HOT 2 CLOSED

Please try this and tell me the result.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.7;
contract C {
enum X { A, B }

X public x;

function f() public returns(uint256) {
uint256 a = 1;
uint256 b = a / a;
X c = X.A;
a = a - a;
b = (b + a / b) >> 1;
a = a + a + a;
a += a * a / a;
if (a > a) a = a + (a - a);
x = c;
return 1;
}

function g() public returns(uint256) {
x = X.A;
return 1;
}

}

from solidity.

Hi, after checking the code and recompiling solc I finally realized that this is a z3 bug. i will close this issue.

from solidity.