Skip to content

Introduce "stride" for range constraints #3148

@chriseth

Description

@chriseth

We lose a lot of information by multiplying a range constraint by a number. Some of that information is kept in the bit masks, but this does not work at all if negative numbers are involved.
If we add another parameter stride, then we could retain all information arising from (non-wrapping) multiplications by numbers, divisions by the same or divisors and arbitrary additions of numbers.
This is especially useful since we don't always know how to normalize affine constraints.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions