SMTChecker: struct variable push() cause false positive

[Subway2023]

Environment

• Compiler version: 0.8.27
• Target EVM version (as per compiler settings): None
• Framework/IDE (e.g. Truffle or Remix): None
• EVM execution environment / backend / blockchain client: None
• Operating system: Linux

Steps to Reproduce

contract C {
    struct S {
        int a;
        bytes5 b;
    }
    S[] b;
    function f() public {
        b.push(S({a: 1, b: "12345"}));
        S[] storage bStorage = b;
        b.push();
        assert(bStorage[0].a == 1);
    }
}

solc b.sol --model-checker-ext-calls trusted --model-checker-timeout 0 --model-checker-engine chc --model-checker-solvers z3

Warning: CHC: Out of bounds access happens here.
  --> test/b.sol:11:16:
   |
11 |         assert(bStorage[0].a == 1);
   |                ^^^^^^^^^^^

Warning: CHC: Assertion violation happens here.
  --> test/b.sol:11:9:
   |
11 |         assert(bStorage[0].a == 1);
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^

If i delete b.push(), there is no false positive