From 2572e1345ed4cc94e96b15945717c4cfed87c19f Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@ethereum.org>
Date: Tue, 23 Apr 2024 13:20:38 +0200
Subject: [PATCH] SMTChecker: Fix equality of array literals

There are two kinds of array literals in Solidity: string literals
(arrays of characters/bytes) and proper array literals (e.g., [1,2,3]).
While array literals cannot be directly tested for equality in Solidity,
it is possible to compute hash of these values and compare hashes.
The expectation is that hashes of the same array literals would be the
same, but previously SMTChecker returned false positive in this case,
saying that they don't have to be equal.

The reason for the false positive was the following.
We represent Solidity array literal as a tuple `(elements, length)` where
`length` is an integer representing the actualy length of the array
literal, and `elements` are an SMT-LIB array, where the first `length`
elements represent the actual content of the array literal.
However, SMT-LIB arrays are infinite objects (more like functions from
indices to elements). Previously, we left the part after `length`-th
element unspecified. For the solver this meant that two array literals
equal at the Solidity level were represented with two different SMT-LIB
arrays.

The proposed solution is to always start from a constant-zero array, and
use store operations to build an SMT-LIB array that matches the Solidity
array literal.
---
 Changelog.md                                  |  1 +
 libsolidity/formal/SMTEncoder.cpp             | 21 ++++++++++++++++-
 .../model_checker_invariants_all/err          |  2 +-
 .../err                                       |  2 +-
 .../abi/abi_encode_packed_string_literal.sol  | 20 +++++++---------
 ...code_packed_string_literal_no_unproved.sol | 20 +++++++---------
 .../abi/abi_encode_string_literal.sol         | 17 ++++++--------
 ...bi_encode_with_selector_string_literal.sol | 21 ++++++++---------
 .../abi/abi_encode_with_sig_array_slice.sol   |  7 ++----
 .../abi/abi_encode_with_sig_array_slice_2.sol |  7 ++----
 .../abi_encode_with_sig_string_literal.sol    | 20 +++++++---------
 .../crypto/crypto_functions_same_array.sol    | 23 +++++++++++++++++++
 .../crypto_functions_same_string_literal.sol  | 23 +++++++++++++++++++
 .../external_calls/call_mutex_unsafe.sol      |  4 ++--
 .../smtCheckerTests/types/array_literal_3.sol |  2 +-
 15 files changed, 116 insertions(+), 74 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_array.sol
 create mode 100644 test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_string_literal.sol

diff --git a/Changelog.md b/Changelog.md
index 59284486b39c..b924b1ccde30 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.