SMTChecker: Underflow and overflow targets not checked or reported on the same expression for BMC engine

[pgebal]

Description

When providing underflow and overflow verification targets only one of them is reported as proved safe for BMC engine.

Environment

• Compiler version: commit 5da0f47

Steps to Reproduce

// SPDX-License-Identifier: GPL-3.0

pragma solidity >=0.0.0;

contract C {
	function f(int x, int y) public pure returns (int) {
		require(x == 0);
		require(y == 0);
		return x + y;
	}
}

then run:

• solc --model-checker-engine bmc --model-checker-targets underflow,overflow test.sol
• solc --model-checker-engine bmc --model-checker-targets underflow test.sol
• solc --model-checker-engine bmc --model-checker-targets overflow test.sol

All The above runs print on output that only 1 verification target was proved correct, although both underflow and overflow should be reported in the first run.

CHC engine is not affected.

[pgebal]

CHC engine is also affected.