diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp
index 56c71f776..0a12059d5 100644
--- a/libsolidity/interface/StandardCompiler.cpp
+++ b/libsolidity/interface/StandardCompiler.cpp
@@ -958,7 +958,7 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 			return formatFatalError("JSONError", "settings.modelChecker.showUnproved must be a Boolean value.");
 		ret.modelCheckerSettings.showUnproved = showUnproved.asBool();
 	}
-	
+
 	if (modelCheckerSettings.isMember("solvers"))
 	{
 		auto const& solversArray = modelCheckerSettings["solvers"];
diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp
index 961baab70..166aa2982 100644
--- a/test/libsolidity/SMTCheckerTest.cpp
+++ b/test/libsolidity/SMTCheckerTest.cpp
@@ -27,6 +27,14 @@ using namespace solidity::frontend::test;
 
 SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, EVMVersion{})
 {
+	auto const& showUnproved = m_reader.stringSetting("SMTShowUnproved", "yes");
+	if (showUnproved == "no")
+		m_modelCheckerSettings.showUnproved = false;
+	else if (showUnproved == "yes")
+		m_modelCheckerSettings.showUnproved = true;
+	else
+		BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT \"show unproved\" choice."));
+
 	auto const& choice = m_reader.stringSetting("SMTSolvers", "any");
 	if (choice == "any")
 		m_modelCheckerSettings.solvers = smtutil::SMTSolverChoice::All();
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol
index 0598311ad..2bbaa2e1c 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol
@@ -22,14 +22,14 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (226-256): CHC: Assertion violation happens here.
 // Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (310-340): CHC: Assertion violation might happen here.
 // Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (483-513): CHC: Assertion violation might happen here.
 // Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (568-598): CHC: Assertion violation might happen here.
 // Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (226-256): CHC: Assertion violation happens here.
+// Warning 6328: (310-340): CHC: Assertion violation might happen here.
+// Warning 6328: (483-513): CHC: Assertion violation might happen here.
+// Warning 6328: (568-598): CHC: Assertion violation might happen here.
 // Warning 6328: (654-684): CHC: Assertion violation might happen here.
 // Warning 4661: (310-340): BMC: Assertion violation happens here.
 // Warning 4661: (483-513): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol
new file mode 100644
index 000000000..ffeef4896
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol
@@ -0,0 +1,35 @@
+contract C {
+	function abiencodePackedStringLiteral() public pure {
+		bytes memory b1 = abi.encodePacked("");
+		bytes memory b2 = abi.encodePacked("");
+		// should hold, but currently fails due to string literal abstraction
+		assert(b1.length == b2.length);
+
+		bytes memory b3 = abi.encodePacked(bytes(""));
+		assert(b1.length == b3.length); // should fail
+
+		bytes memory b4 = abi.encodePacked(bytes24(""));
+		// should hold, but currently fails due to string literal abstraction
+		assert(b1.length == b4.length);
+
+		bytes memory b5 = abi.encodePacked(string(""));
+		assert(b1.length == b5.length); // should fail
+
+		bytes memory b6 = abi.encode("");
+		assert(b1.length == b6.length); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// SMTShowUnproved: no
+// ----
+// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (226-256): CHC: Assertion violation happens here.
+// Warning 5840: CHC: 4 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+// Warning 4661: (310-340): BMC: Assertion violation happens here.
+// Warning 4661: (483-513): BMC: Assertion violation happens here.
+// Warning 4661: (568-598): BMC: Assertion violation happens here.
+// Warning 4661: (654-684): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol
index 6eb3fff73..2a3ff2bb2 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol
@@ -19,12 +19,12 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (208-238): CHC: Assertion violation happens here.
 // Warning 1218: (286-316): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (286-316): CHC: Assertion violation might happen here.
 // Warning 1218: (453-483): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (453-483): CHC: Assertion violation might happen here.
 // Warning 1218: (532-562): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (208-238): CHC: Assertion violation happens here.
+// Warning 6328: (286-316): CHC: Assertion violation might happen here.
+// Warning 6328: (453-483): CHC: Assertion violation might happen here.
 // Warning 6328: (532-562): CHC: Assertion violation might happen here.
 // Warning 4661: (286-316): BMC: Assertion violation happens here.
 // Warning 4661: (453-483): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol
index 0365b9655..c9d9bb056 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol
@@ -25,13 +25,13 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (959-989): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (325-355): CHC: Assertion violation happens here.
 // Warning 6328: (578-608): CHC: Assertion violation happens here.
-// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (691-721): CHC: Assertion violation might happen here.
-// Warning 1218: (959-989): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (959-989): CHC: Assertion violation might happen here.
-// Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (1079-1109): CHC: Assertion violation might happen here.
 // Warning 4661: (691-721): BMC: Assertion violation happens here.
 // Warning 4661: (959-989): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol
index b94977030..740411bf3 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol
@@ -25,13 +25,13 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (692-722): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (960-990): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (326-356): CHC: Assertion violation happens here.
 // Warning 6328: (579-609): CHC: Assertion violation happens here.
-// Warning 1218: (692-722): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (692-722): CHC: Assertion violation might happen here.
-// Warning 1218: (960-990): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (960-990): CHC: Assertion violation might happen here.
-// Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (1080-1110): CHC: Assertion violation might happen here.
 // Warning 4661: (692-722): BMC: Assertion violation happens here.
 // Warning 4661: (960-990): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol
index 3360feb02..ca1b6b40a 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol
@@ -14,8 +14,8 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 1218: (333-371): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (333-371): CHC: Assertion violation might happen here.
 // Warning 1218: (390-428): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (333-371): CHC: Assertion violation might happen here.
 // Warning 6328: (390-428): CHC: Assertion violation might happen here.
 // Warning 4661: (333-371): BMC: Assertion violation happens here.
 // Warning 4661: (390-428): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol
index e824c57d1..839d00835 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol
@@ -22,14 +22,14 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (252-282): CHC: Assertion violation happens here.
 // Warning 1218: (347-377): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (347-377): CHC: Assertion violation might happen here.
 // Warning 1218: (531-561): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (531-561): CHC: Assertion violation might happen here.
 // Warning 1218: (627-657): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (627-657): CHC: Assertion violation might happen here.
 // Warning 1218: (746-776): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (252-282): CHC: Assertion violation happens here.
+// Warning 6328: (347-377): CHC: Assertion violation might happen here.
+// Warning 6328: (531-561): CHC: Assertion violation might happen here.
+// Warning 6328: (627-657): CHC: Assertion violation might happen here.
 // Warning 6328: (746-776): CHC: Assertion violation might happen here.
 // Warning 4661: (347-377): BMC: Assertion violation happens here.
 // Warning 4661: (531-561): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol
index 7530ea6c5..fd15ea27d 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol
@@ -25,13 +25,13 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (702-732): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (971-1001): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (1086-1116): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (334-364): CHC: Assertion violation happens here.
 // Warning 6328: (588-618): CHC: Assertion violation happens here.
-// Warning 1218: (702-732): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (702-732): CHC: Assertion violation might happen here.
-// Warning 1218: (971-1001): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (971-1001): CHC: Assertion violation might happen here.
-// Warning 1218: (1086-1116): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (1086-1116): CHC: Assertion violation might happen here.
 // Warning 4661: (702-732): BMC: Assertion violation happens here.
 // Warning 4661: (971-1001): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol
index f9da7be6b..cdb87233e 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol
@@ -25,13 +25,13 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (703-733): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (972-1002): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (1087-1117): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (335-365): CHC: Assertion violation happens here.
 // Warning 6328: (589-619): CHC: Assertion violation happens here.
-// Warning 1218: (703-733): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (703-733): CHC: Assertion violation might happen here.
-// Warning 1218: (972-1002): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (972-1002): CHC: Assertion violation might happen here.
-// Warning 1218: (1087-1117): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (1087-1117): CHC: Assertion violation might happen here.
 // Warning 4661: (703-733): BMC: Assertion violation happens here.
 // Warning 4661: (972-1002): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol
index a76f91f81..dbf423741 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol
@@ -14,8 +14,8 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 1218: (337-375): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (337-375): CHC: Assertion violation might happen here.
 // Warning 1218: (394-432): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (337-375): CHC: Assertion violation might happen here.
 // Warning 6328: (394-432): CHC: Assertion violation might happen here.
 // Warning 4661: (337-375): BMC: Assertion violation happens here.
 // Warning 4661: (394-432): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol
index 666fa23ba..2e64229bc 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol
@@ -22,14 +22,14 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (261-291): CHC: Assertion violation happens here.
 // Warning 1218: (357-387): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (357-387): CHC: Assertion violation might happen here.
 // Warning 1218: (542-572): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (542-572): CHC: Assertion violation might happen here.
 // Warning 1218: (639-669): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (639-669): CHC: Assertion violation might happen here.
 // Warning 1218: (753-783): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (261-291): CHC: Assertion violation happens here.
+// Warning 6328: (357-387): CHC: Assertion violation might happen here.
+// Warning 6328: (542-572): CHC: Assertion violation might happen here.
+// Warning 6328: (639-669): CHC: Assertion violation might happen here.
 // Warning 6328: (753-783): CHC: Assertion violation might happen here.
 // Warning 4661: (357-387): BMC: Assertion violation happens here.
 // Warning 4661: (542-572): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol
new file mode 100644
index 000000000..02d538d7d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol
@@ -0,0 +1,15 @@
+contract C {
+    struct S {
+        uint x;
+    }
+    S s;
+    function f(bool b) public {
+        s.x |= b ? 1 : 2;
+        assert(s.x > 0);
+    }
+}
+// ====
+// SMTEngine: bmc
+// SMTShowUnproved: no
+// ----
+// Warning 2788: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
index 865ec694b..fd3b55a8c 100644
--- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
+++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
@@ -46,12 +46,12 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 1218: (693-712): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (693-712): CHC: Assertion violation might happen here.
 // Warning 1218: (716-735): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (716-735): CHC: Assertion violation might happen here.
 // Warning 1218: (739-758): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (739-758): CHC: Assertion violation might happen here.
 // Warning 1218: (762-781): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (693-712): CHC: Assertion violation might happen here.
+// Warning 6328: (716-735): CHC: Assertion violation might happen here.
+// Warning 6328: (739-758): CHC: Assertion violation might happen here.
 // Warning 6328: (762-781): CHC: Assertion violation might happen here.
 // Warning 4661: (693-712): BMC: Assertion violation happens here.
 // Warning 4661: (716-735): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
index 3c1777d85..22a4551c8 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
@@ -20,6 +20,5 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 4984: (113-116): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 4984: (113-116): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 6328: (156-170): CHC: Assertion violation happens here.
 // Warning 2661: (113-116): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol
index 7c9ba2d5c..2437d9829 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol
@@ -27,7 +27,6 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 1218: (302-333): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (302-333): CHC: Assertion violation might happen here.
 // Warning 1218: (302-333): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (302-333): CHC: Assertion violation might happen here.
 // Warning 4661: (302-333): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/file_level/recursion.sol b/test/libsolidity/smtCheckerTests/file_level/recursion.sol
index f461861e9..34a26d326 100644
--- a/test/libsolidity/smtCheckerTests/file_level/recursion.sol
+++ b/test/libsolidity/smtCheckerTests/file_level/recursion.sol
@@ -25,4 +25,3 @@ contract C {
 }
 // ====
 // SMTEngine: all
-// ----
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol
index 067ac0218..84fdaf87d 100644
--- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol
@@ -21,5 +21,5 @@ contract A is B {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 6328: (200-218): CHC: Assertion violation happens here.
 // Warning 4984: (171-176): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (200-218): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol
index 165740218..b7cacc0f6 100644
--- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol
@@ -19,5 +19,5 @@ contract A is B {
 // ====
 // SMTEngine: all
 // ----
-// Warning 4984: (175-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\nTransaction trace:\nA.constructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
 // Warning 4984: (166-171): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639934\n\nTransaction trace:\nA.constructor(115792089237316195423570985008687907853269984665640564039457584007913129639934)
+// Warning 4984: (175-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\nTransaction trace:\nA.constructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol
index 98da0a2a6..6a2b07919 100644
--- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol
@@ -29,6 +29,6 @@ contract A is B2, B1 {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 4984: (209-214): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (193-198): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (209-214): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (302-318): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
index 414809209..8fd9bf9a2 100644
--- a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
@@ -14,5 +14,5 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 6328: (129-143): CHC: Assertion violation happens here.
 // Warning 4984: (82-87): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (129-143): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol
index cf31fa9e5..1fe537aad 100644
--- a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol
+++ b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol
@@ -21,8 +21,8 @@ contract C{
 // SMTEngine: all
 // ----
 // Warning 5667: (37-43): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0)
 // Warning 6328: (105-119): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()
 // Warning 6328: (137-151): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n    C.g() -- internal call
 // Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n    C.g() -- internal call
 // Warning 6328: (212-226): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n    C.g() -- internal call
-// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0)
diff --git a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol
index 2e934a0f2..f03e1b4eb 100644
--- a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol
+++ b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol
@@ -21,6 +21,6 @@ contract C{
 // SMTEngine: all
 // ----
 // Warning 5667: (37-43): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0)
 // Warning 6328: (105-119): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()
 // Warning 6328: (151-165): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n    C.g() -- internal call\n    C.g() -- internal call
-// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0)
diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol
index 83f8e609c..f97bae5cd 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol
@@ -28,5 +28,5 @@ contract C is B {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()\n    A.v() -- internal call
 // Warning 6328: (62-76): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nB.f()\n    A.f() -- internal call\n        C.v() -- internal call
+// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()\n    A.v() -- internal call
diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol
index f3a6393fa..f02e416a4 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol
@@ -23,6 +23,6 @@ contract A is B {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 6328: (243-261): CHC: Assertion violation happens here.
 // Warning 4984: (125-130): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (184-189): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (243-261): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol
index d20358525..e223ad5f7 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol
@@ -23,6 +23,6 @@ contract A is B {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 6328: (241-259): CHC: Assertion violation happens here.
 // Warning 4984: (125-131): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (185-190): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (241-259): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol
index 940ff64b3..c7c63f00f 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol
@@ -25,5 +25,5 @@ contract D is B, C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (223-237): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor()
 // Warning 6328: (134-148): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nD.constructor()
+// Warning 6328: (223-237): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor()
diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol
index 88fe7f51f..02a66575a 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol
@@ -24,5 +24,5 @@ contract LoopFor2 {
 // ----
 // Warning 2072: (202-217): Unused local variable.
 // Warning 6368: (354-358): CHC: Out of bounds access happens here.
-// Warning 6368: (378-382): CHC: Out of bounds access happens here.
 // Warning 6368: (371-375): CHC: Out of bounds access happens here.
+// Warning 6368: (378-382): CHC: Out of bounds access happens here.
diff --git a/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol
index dc4fc9ef1..2a2f16c47 100644
--- a/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol
+++ b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol
@@ -35,4 +35,3 @@ contract C {
 }
 // ====
 // SMTEngine: chc
-// ----
diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
index e617e274e..d7a309405 100644
--- a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
+++ b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
@@ -7,5 +7,5 @@ contract C  {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 4281: (77-82): CHC: Division by zero happens here.
 // Warning 4984: (77-82): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
+// Warning 4281: (77-82): CHC: Division by zero happens here.
diff --git a/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol b/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol
index f1bcf66b6..efc59fcfc 100644
--- a/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol
+++ b/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol
@@ -14,5 +14,5 @@ contract C is A {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (240-254): CHC: Assertion violation happens here.\nCounterexample:\nv = 1, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 }
 // Warning 6328: (60-74): CHC: Assertion violation happens here.\nCounterexample:\nv = 0, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 }
+// Warning 6328: (240-254): CHC: Assertion violation happens here.\nCounterexample:\nv = 1, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 }
diff --git a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_function_call.sol b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_function_call.sol
index 10fd28ee3..7ce444357 100644
--- a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_function_call.sol
+++ b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_function_call.sol
@@ -11,5 +11,5 @@ contract B {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 6328: (130-152): CHC: Assertion violation happens here.
 // Warning 6328: (104-126): CHC: Assertion violation happens here.
+// Warning 6328: (130-152): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol b/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol
new file mode 100644
index 000000000..6ec629c9f
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol
@@ -0,0 +1,25 @@
+contract C
+{
+	uint[][][] c;
+	constructor() {
+		c.push();
+		c[0].push();
+		c[0][0].push();
+	}
+	function f(bool b) public {
+		c[0][0][0] = 0;
+		if (b)
+			c[0][0][0] = 1;
+		assert(c[0][0][0] < 2);
+	}
+}
+// ====
+// SMTEngine: all
+// SMTShowUnproved: yes
+// ----
+// Warning 6368: (124-131): CHC: Out of bounds access might happen here.
+// Warning 6368: (124-134): CHC: Out of bounds access might happen here.
+// Warning 6368: (152-159): CHC: Out of bounds access might happen here.
+// Warning 6368: (152-162): CHC: Out of bounds access might happen here.
+// Warning 6368: (177-184): CHC: Out of bounds access might happen here.
+// Warning 6368: (177-187): CHC: Out of bounds access might happen here.
diff --git a/test/solc/CommandLineParser.cpp b/test/solc/CommandLineParser.cpp
index 02444ce5d..bb427232c 100644
--- a/test/solc/CommandLineParser.cpp
+++ b/test/solc/CommandLineParser.cpp
@@ -82,6 +82,7 @@ BOOST_AUTO_TEST_CASE(no_options)
 	expectedOptions.modelChecker.settings = {
 		ModelCheckerContracts::Default(),
 		ModelCheckerEngine::None(),
+		false,
 		smtutil::SMTSolverChoice::All(),
 		ModelCheckerTargets::Default(),
 		nullopt,
@@ -151,6 +152,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options)
 			"--yul-optimizations=agf",
 			"--model-checker-contracts=contract1.yul:A,contract2.yul:B",
 			"--model-checker-engine=bmc",
+			"--model-checker-show-unproved=true",
 			"--model-checker-solvers=z3,smtlib2",
 			"--model-checker-targets=underflow,divByZero",
 			"--model-checker-timeout=5",
@@ -209,6 +211,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options)
 		expectedOptions.modelChecker.settings = {
 			{{{"contract1.yul", {"A"}}, {"contract2.yul", {"B"}}}},
 			{true, false},
+			true,
 			{false, true, true},
 			{{VerificationTargetType::Underflow, VerificationTargetType::DivByZero}},
 			5,
@@ -279,6 +282,7 @@ BOOST_AUTO_TEST_CASE(assembly_mode_options)
 				"contract1.yul:A,"
 				"contract2.yul:B",
 			"--model-checker-engine=bmc",  // Ignored in assembly mode
+			"--model-checker-show-unproved=true", // Ignored in assembly mode
 			"--model-checker-solvers=z3,smtlib2", // Ignored in assembly mode
 			"--model-checker-targets="     // Ignored in assembly mode
 				"underflow,"
@@ -377,6 +381,7 @@ BOOST_AUTO_TEST_CASE(standard_json_mode_options)
 			"contract1.yul:A,"
 			"contract2.yul:B",
 		"--model-checker-engine=bmc",      // Ignored in Standard JSON mode
+		"--model-checker-show-unproved=true",      // Ignored in Standard JSON mode
 		"--model-checker-solvers=z3,smtlib2", // Ignored in Standard JSON mode
 		"--model-checker-targets="         // Ignored in Standard JSON mode
 			"underflow,"