Skip to content

Incorrect SMT2 generation when using C structs #398

Closed
@david-k

Description

@david-k

The following program is correctly verified by CBMC but fails with Z3 (outputs sat) using the generated SMT2 file:

typedef struct
{
	char val;
} Struct;

int main()
{
	char a;
	Struct r;
	r.val = a;

	__CPROVER_assert(r.val == a, "equal");
}

On the other hand, if you directly initialize r (Struct r = {a};) then Z3 outputs the correct result. The SMT2 file is a bit above my head so I couldn't really figure out what's wrong.

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