diff --git a/Changelog.md b/Changelog.md
index c118e9f248a4..ab767b64664a 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -9,6 +9,7 @@ Compiler Features:
 
 Bugfixes:
  * Commandline Interface: Fix ICE when the optimizer is disabled and an empty/blank string is used for ``--yul-optimizations`` sequence.
+ * SMTChecker: Fix false positive when comparing hashes of same array or string literals.
  * SMTChecker: Fix internal error on mapping access caused by too strong requirements on sort compatibility of the index and mapping domain.
  * SMTChecker: Fix internal error when using an empty tuple in a conditional operator.
  * SMTChecker: Fix internal error when using bitwise operators with an array element as argument.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 61aad0e8f526..c92c5399a685 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1296,8 +1296,27 @@ void SMTEncoder::addArrayLiteralAssertions(
 )
 {
 	m_context.addAssertion(_symArray.length() == _elementValues.size());
+
+	// Assert to the solver that _elementValues are exactly the elements at the beginning of the array.
+	// Since we create new symbolic representation for every array literal in the source file, we want to ensure that
+	// representations of two equal literals are also equal. For this reason we always start from constant-zero array.
+	// This ensures SMT-LIB arrays (which are infinite) are also equal beyond the length of the Solidity array literal.
+	auto type = _symArray.type();
+	smtAssert(type);
+	auto valueType = [&]() {
+		if (auto const* arrayType = dynamic_cast<ArrayType const*>(type))
+			return arrayType->baseType();
+		if (smt::isStringLiteral(*type))
+			return TypeProvider::stringMemory()->baseType();
+		smtAssert(false);
+	}();
+	auto tupleSort = std::dynamic_pointer_cast<smtutil::TupleSort>(smt::smtSort(*type));
+	auto sortSort = std::make_shared<smtutil::SortSort>(tupleSort->components.front());
+	smtutil::Expression arrayExpr = smtutil::Expression::const_array(smtutil::Expression(sortSort), smt::zeroValue(valueType));
+	smtAssert(arrayExpr.sort->kind == smtutil::Kind::Array);
 	for (size_t i = 0; i < _elementValues.size(); i++)
-		m_context.addAssertion(smtutil::Expression::select(_symArray.elements(), i) == _elementValues[i]);
+		arrayExpr = smtutil::Expression::store(arrayExpr, smtutil::Expression(i), _elementValues[i]);
+	m_context.addAssertion(_symArray.elements() == arrayExpr);
 }
 
 void SMTEncoder::bytesToFixedBytesAssertions(
diff --git a/test/cmdlineTests/model_checker_invariants_all/err b/test/cmdlineTests/model_checker_invariants_all/err
index 347f40325d14..7ec97678e990 100644
--- a/test/cmdlineTests/model_checker_invariants_all/err
+++ b/test/cmdlineTests/model_checker_invariants_all/err
@@ -9,6 +9,6 @@ Info: CHC: 1 verification condition(s) proved safe! Enable the model checker opt
 Info: Contract invariant(s) for model_checker_invariants_all/input.sol:test:
 (!(x >= 1) || true)
 Reentrancy property(ies) for model_checker_invariants_all/input.sol:test:
-(((!(x <= 0) || !(x' >= 1)) && (!(x <= 0) || !(<errorCode> >= 1))) || true)
+(((!(x <= 0) || !(<errorCode> >= 1)) && (!(x <= 0) || !(x' >= 1))) || true)
 <errorCode> = 0 -> no errors
 <errorCode> = 1 -> Assertion failed at assert(x == 0)
diff --git a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err
index c6d149f15a40..11ee3a702f8c 100644
--- a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err
+++ b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err
@@ -9,6 +9,6 @@ Info: CHC: 1 verification condition(s) proved safe! Enable the model checker opt
 Info: Contract invariant(s) for model_checker_invariants_contract_reentrancy/input.sol:test:
 (!(x >= 1) || true)
 Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test:
-(((!(x <= 0) || !(x' >= 1)) && (!(x <= 0) || !(<errorCode> >= 1))) || true)
+(((!(x <= 0) || !(<errorCode> >= 1)) && (!(x <= 0) || !(x' >= 1))) || true)
 <errorCode> = 0 -> no errors
 <errorCode> = 1 -> Assertion failed at assert(x == 0)
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 08c48cbd99de..47b15369c04c 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol
@@ -2,18 +2,16 @@ 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);
+		assert(b1.length == b2.length); // should hold
 
 		bytes memory b3 = abi.encodePacked(bytes(""));
-		assert(b1.length == b3.length); // should fail
+		assert(b1.length == b3.length); // should hold
 
 		bytes memory b4 = abi.encodePacked(bytes24(""));
-		// should hold, but currently fails due to string literal abstraction
-		assert(b1.length == b4.length);
+		assert(b1.length == b4.length); // should fail
 
 		bytes memory b5 = abi.encodePacked(string(""));
-		assert(b1.length == b5.length); // should fail
+		assert(b1.length == b5.length); // should hold, but currently fails due to abstraction
 
 		bytes memory b6 = abi.encode("");
 		assert(b1.length == b6.length); // should fail
@@ -21,10 +19,8 @@ contract C {
 }
 // ====
 // SMTEngine: all
-// SMTIgnoreOS: macos
 // ----
-// Warning 6328: (226-256): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = [0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42]\nb3 = []\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
-// Warning 6328: (310-340): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72]\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
-// Warning 6328: (483-513): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
-// Warning 6328: (568-598): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc]\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
-// Warning 6328: (654-684): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a]\nb6 = [0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117]\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
+// Warning 6328: (354-384): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
+// Warning 6328: (454-484): CHC: Assertion violation happens here.\nCounterexample:\n\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
+// Warning 6328: (580-610): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
+// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
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
index f80027626102..581e649fcbbe 100644
--- 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
@@ -2,18 +2,16 @@ 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);
+		assert(b1.length == b2.length); // should hold
 
 		bytes memory b3 = abi.encodePacked(bytes(""));
-		assert(b1.length == b3.length); // should fail
+		assert(b1.length == b3.length); // should hold
 
 		bytes memory b4 = abi.encodePacked(bytes24(""));
-		// should hold, but currently fails due to string literal abstraction
-		assert(b1.length == b4.length);
+		assert(b1.length == b4.length); // should fail
 
 		bytes memory b5 = abi.encodePacked(string(""));
-		assert(b1.length == b5.length); // should fail
+		assert(b1.length == b5.length); // should hold, but fails due to abstraction
 
 		bytes memory b6 = abi.encode("");
 		assert(b1.length == b6.length); // should fail
@@ -22,10 +20,8 @@ contract C {
 // ====
 // SMTEngine: all
 // SMTShowUnproved: no
-// SMTIgnoreOS: macos
 // ----
-// Warning 6328: (226-256): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = [0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42]\nb3 = []\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
-// Warning 6328: (310-340): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72]\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
-// Warning 6328: (483-513): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
-// Warning 6328: (568-598): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc]\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
-// Warning 6328: (654-684): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a]\nb6 = [0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117]\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
+// Warning 6328: (354-384): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
+// Warning 6328: (454-484): CHC: Assertion violation happens here.\nCounterexample:\n\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
+// Warning 6328: (570-600): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
+// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol
index b55952ee74f6..77d3cfb83be4 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol
@@ -2,25 +2,22 @@ contract C {
 	function abiEncodeStringLiteral() public pure {
 		bytes memory b1 = abi.encode("");
 		bytes memory b2 = abi.encode("");
-		// should hold, but currently fails due to string literal abstraction
+		// should hold
 		assert(b1.length == b2.length);
 
 		bytes memory b3 = abi.encode(bytes(""));
-		assert(b1.length == b3.length); // should fail
+		assert(b1.length == b3.length); // should hold
 
 		bytes memory b4 = abi.encode(bytes24(""));
-		// should hold, but currently fails due to string literal abstraction
-		assert(b1.length == b4.length);
+		assert(b1.length == b4.length); // should fail
 
 		bytes memory b5 = abi.encode(string(""));
-		assert(b1.length == b5.length); // should fail
+		assert(b1.length == b5.length); // should hold, but currently fails due to abstraction
 	}
 }
 // ====
 // SMTEngine: all
-// SMTIgnoreOS: macos
 // ----
-// Warning 6328: (208-238): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = []\nb4 = []\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
-// Warning 6328: (286-316): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d]\nb3 = [0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d]\nb4 = []\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
-// Warning 6328: (453-483): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
-// Warning 6328: (532-562): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca]\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
+// Warning 6328: (326-356): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
+// Warning 6328: (420-450): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
+// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
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 6d1ab3066c84..dd183263a42f 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
@@ -2,18 +2,17 @@ contract C {
 	function abiEncodeStringLiteral(bytes4 sel) public pure {
 		bytes memory b1 = abi.encodeWithSelector(sel, "");
 		bytes memory b2 = abi.encodeWithSelector(sel, "");
-		// should hold, but currently fails due to string literal abstraction
-		assert(b1.length == b2.length);
+
+		assert(b1.length == b2.length); // should hold
 
 		bytes memory b3 = abi.encodeWithSelector(sel, bytes(""));
-		assert(b1.length == b3.length); // should fail
+		assert(b1.length == b3.length); // should hold
 
 		bytes memory b4 = abi.encodeWithSelector(sel, bytes24(""));
-		// should hold, but currently fails due to string literal abstraction
-		assert(b1.length == b4.length);
+		assert(b1.length == b4.length); // should fail
 
 		bytes memory b5 = abi.encodeWithSelector(sel, string(""));
-		assert(b1.length == b5.length); // should fail
+		assert(b1.length == b5.length); // should hold, but currently fails due to abstraction
 
 		bytes memory b6 = abi.encodeWithSelector(0xcafecafe, bytes24(""));
 		assert(b4.length == b6.length); // should fail
@@ -21,10 +20,8 @@ contract C {
 }
 // ====
 // SMTEngine: all
-// SMTIgnoreOS: macos
 // ----
-// Warning 6328: (252-282): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb1 = [0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46]\nb3 = []\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
-// Warning 6328: (347-377): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb3 = [0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d]\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
-// Warning 6328: (531-561): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb1 = [0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90]\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
-// Warning 6328: (627-657): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb5 = [0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1]\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
-// Warning 6328: (746-776): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb2 = []\nb5 = [0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2]\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
+// Warning 6328: (403-433): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
+// Warning 6328: (514-544): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
+// Warning 6328: (673-703): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
+// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
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 fad7437448f3..b2d1b4acc6d0 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
@@ -24,10 +24,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
-// SMTIgnoreOS: macos
 // ----
-// Warning 6328: (334-364): CHC: Assertion violation happens here.
+// Warning 6328: (334-364): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [0x4f]\nb2 = [0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c, 0x5c]\nb3 = []\nb4 = []\nx = 0\ny = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSlice(sig, [0x4f]) -- counterexample incomplete; parameter name used instead of value
 // Warning 6328: (588-618): CHC: Assertion violation happens here.
-// Warning 6328: (1086-1116): CHC: Assertion violation might happen here.
-// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
-// Warning 4661: (1086-1116): BMC: Assertion violation happens here.
+// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
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 41e71ee5bf0e..4c21a02a6bbb 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
@@ -24,10 +24,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
-// SMTIgnoreOS: macos
 // ----
-// Warning 6328: (335-365): CHC: Assertion violation happens here.
+// Warning 6328: (335-365): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [36]\nb3 = []\nb4 = []\nx = 0\ny = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSlice(sig, [36]) -- counterexample incomplete; parameter name used instead of value
 // Warning 6328: (589-619): CHC: Assertion violation happens here.
-// Warning 6328: (1087-1117): CHC: Assertion violation might happen here.
-// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
-// Warning 4661: (1087-1117): BMC: Assertion violation happens here.
+// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
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 de218cfaa6d6..ca782442b6f1 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
@@ -2,18 +2,16 @@ contract C {
 	function abiEncodeStringLiteral(string memory sig) public pure {
 		bytes memory b1 = abi.encodeWithSignature(sig, "");
 		bytes memory b2 = abi.encodeWithSignature(sig, "");
-		// should hold, but currently fails due to string literal abstraction
-		assert(b1.length == b2.length);
+		assert(b1.length == b2.length); // should hold
 
 		bytes memory b3 = abi.encodeWithSignature(sig, bytes(""));
-		assert(b1.length == b3.length); // should fail
+		assert(b1.length == b3.length); // should hold
 
 		bytes memory b4 = abi.encodeWithSignature(sig, bytes24(""));
-		// should hold, but currently fails due to string literal abstraction
-		assert(b1.length == b4.length);
+		assert(b1.length == b4.length); // should fail
 
 		bytes memory b5 = abi.encodeWithSignature(sig, string(""));
-		assert(b1.length == b5.length); // should fail
+		assert(b1.length == b5.length); // should hold, but currently fails due to abstraction
 
 		bytes memory b6 = abi.encodeWithSelector("f()", bytes24(""));
 		assert(b4.length == b6.length); // should fail
@@ -21,10 +19,8 @@ contract C {
 }
 // ====
 // SMTEngine: all
-// SMTIgnoreOS: macos
 // ----
-// Warning 6328: (261-291): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a]\nb3 = []\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(sig)
-// Warning 6328: (357-387): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90]\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(sig)
-// Warning 6328: (542-572): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa]\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(sig)
-// Warning 6328: (639-669): CHC: Assertion violation happens here.\nCounterexample:\n\nb4 = [0x22, 0x22, 0x22, 0x22, 0x22, 0x0d, 0x22, 0x22, 0x22, 0x22, 0x09, 0x22, 0x0b, 0x22, 0x22, 0x0e, 0x22, 0x10, 0x22, 0x12, 0x22, 0x14, 0x22, 0x16, 0x22, 0x18, 0x22, 0x1a, 0x22, 0x1c, 0x22, 0x1e, 0x22, 0x20, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22]\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(sig)
-// Warning 6328: (753-783): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117]\nb4 = []\nb5 = [0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118]\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(sig)
+// Warning 6328: (413-443): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(sig) -- counterexample incomplete; parameter name used instead of value
+// Warning 6328: (525-555): CHC: Assertion violation happens here.\nCounterexample:\n\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(sig) -- counterexample incomplete; parameter name used instead of value
+// Warning 6328: (679-709): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(sig) -- counterexample incomplete; parameter name used instead of value
+// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_array.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_array.sol
new file mode 100644
index 000000000000..b0e3b9565aab
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_array.sol
@@ -0,0 +1,23 @@
+contract C {
+	function c1() public pure {
+		bytes32 k1 = keccak256(abi.encode([1]));
+		bytes32 k2 = keccak256(abi.encode([1]));
+		assert(k1 == k2);
+	}
+
+        function c2() public pure {
+		bytes32 s1 = sha256(abi.encode([1,2]));
+		bytes32 s2 = sha256(abi.encode([1,2]));
+		assert(s1 == s2);
+	}
+
+        function c3() public pure {
+		bytes32 r1 = ripemd160(abi.encode([1,2,3]));
+		bytes32 r2 = ripemd160(abi.encode([1,2,3]));
+		assert(r1 == r2);
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_string_literal.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_string_literal.sol
new file mode 100644
index 000000000000..9e5123ab5bd5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_string_literal.sol
@@ -0,0 +1,23 @@
+contract C {
+	function c1() public pure {
+		bytes32 k1 = keccak256("1");
+		bytes32 k2 = keccak256("1");
+		assert(k1 == k2);
+	}
+
+        function c2() public pure {
+		bytes32 s1 = sha256("10");
+		bytes32 s2 = sha256("10");
+		assert(s1 == s2);
+	}
+
+        function c3() public pure {
+		bytes32 r1 = ripemd160("100");
+		bytes32 r2 = ripemd160("100");
+		assert(r1 == r2);
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol b/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol
index e8c17d3eb05f..d2fefcd5f743 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol
@@ -21,7 +21,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
-// SMTIgnoreCex: no
+// SMTIgnoreCex: yes
 // ----
 // Warning 9302: (212-228): Return value of low-level calls not used.
-// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, lock = false\n_a = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.set(1)\nState: x = 1, lock = false\nC.f(0x0)\n    _a.call("aaaaa") -- untrusted external call, synthesized as:\n        C.set(0) -- reentrant call
+// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, lock = false\n_a = 0x0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.f(0x0)\n    _a.call("aaaaa") -- untrusted external call, synthesized as:\n        C.set(1) -- reentrant call
diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_3.sol b/test/libsolidity/smtCheckerTests/types/array_literal_3.sol
index cdaff2bf44a4..b4655f394f83 100644
--- a/test/libsolidity/smtCheckerTests/types/array_literal_3.sol
+++ b/test/libsolidity/smtCheckerTests/types/array_literal_3.sol
@@ -11,5 +11,5 @@ contract C
 // SMTEngine: all
 // SMTIgnoreCex: no
 // ----
-// Warning 6328: (168-188): CHC: Assertion violation happens here.
+// Warning 6328: (168-188): CHC: Assertion violation happens here.\nCounterexample:\n\na = [1, 2, 3]\nb = [1, 2, 4]\n\nTransaction trace:\nC.constructor()\nC.f()
 // Info 1391: CHC: 8 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.