diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 912e2a69b..78591ad69 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -1371,7 +1371,7 @@ void SMTChecker::createExpr(Expression const& _e) void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) { createExpr(_e); - solAssert(isSupportedType(*_e.annotation().type), "Equality operator applied to type that is not fully supported"); + solAssert(smtKind(_e.annotation().type->category()) != smt::Kind::Function, "Equality operator applied to type that is not fully supported"); m_interface->addAssertion(expr(_e) == _value); } diff --git a/test/libsolidity/smtCheckerTests/types/struct_1.sol b/test/libsolidity/smtCheckerTests/types/struct_1.sol new file mode 100644 index 000000000..0cc5b1e41 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct_1.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; + +contract C +{ + struct S { + uint x; + } + + mapping (uint => S) smap; + + function f(uint y, uint v) public { + smap[y] = S(v); + S memory smem = S(v); + } +} +// ---- +// Warning: (157-170): Unused local variable. +// Warning: (157-170): Assertion checker does not yet support the type of this variable. +// Warning: (139-146): Assertion checker does not yet implement this type. +// Warning: (149-153): Assertion checker does not yet implement this expression. +// Warning: (139-153): Assertion checker does not yet implement type struct C.S storage ref +// Warning: (173-177): Assertion checker does not yet implement this expression. +// Warning: (173-177): Internal error: Expression undefined for SMT solver. +// Warning: (173-177): Assertion checker does not yet implement this type.