SMTChecker: Fix parsing bv2int expression from solver's response

libsmtutil/CHCSmtLib2Interface.cpp

@@ -365,6 +365,11 @@ smtutil::Expression CHCSmtLib2Interface::ScopedParser::toSMTUtilExpression(SMTLi
 						smtSolverInteractionRequire(arguments.size() == 3, "Store has three arguments: array, index and element");
 						return smtutil::Expression::store(arguments[0], arguments[1], arguments[2]);
 					}
+					if (op == "bv2int")
+					{
+						smtSolverInteractionRequire(arguments.size() == 1, "bv2int has one argument");
+						return smtutil::Expression::bv2int(arguments[0]);
+					}
 					else
 					{
 						std::set<std::string> boolOperators{"and", "or", "not", "=", "<", ">", "<=", ">=", "=>"};

test/libsolidity/smtCheckerTests/invariants/solver_response_involves_bv2int.sol

@@ -0,0 +1,16 @@
+// Taken from issue #15770
+contract c {
+    function f(uint len) public pure returns (bytes memory) {
+        bytes memory x = new bytes(len);
+        for (uint i = 0; i < len; i++) {
+            x[i] = bytes1(uint8(i));
+        }
+        return x;
+    }
+}
+// ====
+// SMTEngine: chc
+// SMTIgnoreInv: no
+// SMTSolvers: z3
+// ----
+// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.