[SMTChecker] correct handling of FixedBytes constants initialized with string literal

Author: Martin Blicha

Changelog.md

@@ -7,8 +7,8 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Fix internal error on ``FixedBytes`` constant initialized with string literal.
  * SMTChecker: Fix internal error on pushing to ``string`` casted to ``bytes``.
-
 AST Changes:
 
 

libsmtutil/SolverInterface.h

@@ -260,6 +260,7 @@ class Expression
 	}
 	friend Expression operator==(Expression _a, Expression _b)
 	{
+		smtAssert(_a.sort->kind == _b.sort->kind, "Trying to create an 'equal' expression with different sorts");
 		return Expression("=", std::move(_a), std::move(_b), Kind::Bool);
 	}
 	friend Expression operator!=(Expression _a, Expression _b)

libsolidity/formal/SMTEncoder.cpp

@@ -940,7 +940,7 @@ void SMTEncoder::endVisit(Identifier const& _identifier)
 			{
 				solAssert(decl->value(), "");
 				decl->value()->accept(*this);
-				defineExpr(_identifier, expr(*decl->value()));
+				defineExpr(_identifier, expr(*decl->value(), _identifier.annotation().type));
 			}
 		}
 		else

test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_constant_initialization_1.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract MockContract {
+	bytes4 public constant SENTINEL_ANY_MOCKS = hex"01";
+	mapping(bytes4 => bytes4) methodIdMocks;
+
+	constructor() {
+		methodIdMocks[SENTINEL_ANY_MOCKS] = 0;
+	}
+}

test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_constant_initialization_2.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract MockContract {
+	bytes4 public constant SENTINEL_ANY_MOCKS = hex"01";
+
+	constructor() {
+		assert(SENTINEL_ANY_MOCKS >= 0);
+	}
+}