SMTChecker: Fix string literal to fixed bytes conversion with user-defined type

Author: blishko

Changelog.md

@@ -8,6 +8,7 @@ Compiler Features:
 
 Bugfixes:
 * SMTChecker: Fix incorrect analysis when only a subset of contracts is selected with `--model-checker-contracts`.
+* SMTChecker: Fix internal compiler error when string literal is used to initialize user-defined type based on fixed bytes.
 
 
 ### 0.8.29 (2025-03-12)

libsolidity/formal/SMTEncoder.cpp

@@ -929,8 +929,10 @@ void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall)
 void SMTEncoder::visitWrapUnwrap(FunctionCall const& _funCall)
 {
 	auto const& args = _funCall.arguments();
-	solAssert(args.size() == 1, "");
-	defineExpr(_funCall, expr(*args.front()));
+	smtAssert(args.size() == 1, "Expected exactly one argument to wrap/unwrap");
+	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	auto const* argType = funType.parameterTypes().front();
+	defineExpr(_funCall, expr(*args.front(), argType));
 }
 
 void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)

test/libsolidity/smtCheckerTests/userTypes/user_type_over_fixed_bytes_can_be_initialized_from_string_literal.sol

@@ -0,0 +1,15 @@
+type MyBytes is bytes2;
+
+contract C {
+    MyBytes b = MyBytes.wrap("ab");
+
+    function check() view public {
+        assert(MyBytes.unwrap(b) == 0); // should fail
+        assert(MyBytes.unwrap(b) == 0x6162); // should hold
+    }
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 6328: (118-148): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.check()
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.