Skip to content

Support for typecasting between 2 types of arrays is not yet implemented in incremental smt2 decision procedure #8075

@esteffin

Description

@esteffin

Support for typecasting between 2 types of arrays is not yet implemented in incremental smt2 decision procedure.

This causes a failure with invariant stating that it's not possible to typecast an array of type signed_bv of 32 bits and size 4 to an array of type signed_bv of 64 bits and size 2.

This is required for the following test:

  • cbmc/SIMD1/test.desc

Note that to get this error the test should be run on a x86_64 CPU supporting __MMX__.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions