Skip to content

[SMT] Implicit overflow when parsing !smt.bv type? #8062

Open
@maerhart

Description

When providing the following as input to circt-opt

hw.module @ImplicitOverflow() {
  %0 = smt.bv.constant #smt.bv<1> : !smt.bv<18446744073709551615>
}

it outputs

hw.module @ImplicitOverflow() {
  %c1_bv4294967295 = smt.bv.constant #smt.bv<1> : !smt.bv<4294967295>
  hw.output
}

Using !smt.bv<18446744073709551616> as input expectedly triggers an error that the integer is too large.
Seems like we store it in some 32 bit integer at some point?

Metadata

Assignees

No one assigned

    Labels

    SMTbugSomething isn't working

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions