Merge pull request #14988 from pgebal/smt_chcecker_fix_internal_error…

…_on_bitwise

SMTChecker: Fix internal error when using bitwise operators with an array as argument

Changelog.md

@@ -7,6 +7,7 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Fix internal error when using bitwise operators with an array element as argument.
 
 
 ### 0.8.25 (2023-03-14)

libsmtutil/Z3Interface.cpp

@@ -386,6 +386,8 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
 		kind == Z3_OP_RECURSIVE
 	)
 		return Expression(_expr.decl().name().str(), arguments, fromZ3Sort(_expr.get_sort()));
+	else if (kind == Z3_OP_CONCAT)
+		return Expression("concat", arguments, sort);
 
 	smtAssert(false);
 

test/libsolidity/smtCheckerTests/operators/bitwise_and_array.sol

@@ -0,0 +1,17 @@
+contract C {
+	function bitwiseXor(int[10] memory p) public pure {
+        1 ^ p[0];
+	}
+
+	function bitwiseAnd(int[10] memory p) public pure {
+		1 & p[0];
+	}
+
+	function bitwiseOr(int[10] memory p) public pure {
+		1 | p[0];
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.