solidity icon indicating copy to clipboard operation
solidity copied to clipboard

SMTChecker: Fix crash on mappings

Open blishko opened this issue 1 year ago • 0 comments

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.

blishko avatar Feb 09 '24 15:02 blishko