SMTChecker: Z3 in CHC engine incorrectly determines assertion as safe, when it should report possible violation

[blishko]

Input

contract C {
	function abiEncodeSlice(bytes4 sel, uint[] calldata data) external pure {
		bytes memory b1 = abi.encodeWithSelector(sel, data);
		bytes memory b2 = abi.encodeWithSelector(sel, data[0:]);
		assert(b1.length == b2.length);

		bytes memory b3 = abi.encodeWithSelector(sel, data[:data.length]);
		assert(b1.length == b3.length);

		bytes memory b4 = abi.encodeWithSelector(sel, data[5:10]);
		assert(b1.length == b4.length); // should fail
	}
}

Command line options: --model-checker-engine chc --model-checker-solvers z3

Actual output

Warning: CHC: Assertion violation happens here.
 --> bug.sol:5:3:
  |
5 | 		assert(b1.length == b2.length);
  | 		^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Warning: CHC: Assertion violation happens here.
 --> bug.sol:8:3:
  |
8 | 		assert(b1.length == b3.length);
  | 		^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

Expected output, which is correctly reported by Eldarica (--model-checker-solvers eld):

Warning: CHC: Assertion violation happens here.
 --> bug.sol:5:3:
  |
5 | 		assert(b1.length == b2.length);
  | 		^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Warning: CHC: Assertion violation happens here.
 --> bug.sol:8:3:
  |
8 | 		assert(b1.length == b3.length);
  | 		^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Warning: CHC: Assertion violation happens here.
  --> bug.sol:11:3:
   |
11 | 		assert(b1.length == b4.length); // should fail
   | 		^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This is a slightly simplified version of the file abi/abi_encode_array_slice_2.sol in SMTChecker test suite.