solidity
solidity copied to clipboard
SMTChecker: Fix crash on mappings
Previously, creating zero value expression for integer type (solidity::frontend::IntegerType) did not respect signedness of the type. This led to an assertion violation in methods creating SMT representation of array expressions, which have strict type checks.
We fix the issues by correctly constructing either signed or unsigned SMT expression representing zero based on the sign of the provided integer type.
Fixes #14791. Fixes #14792.