inconsistencies with structs


The following verifies with the switch /z:MBQI=true:
(struct P {} ;)
void test() { _(assert \false) }
The following also verifies (with the same switches):

typedef struct S { int x; } S;
void test() {  S s; _(assert \false) }

file attachments


erniecohen wrote Aug 27, 2015 at 2:11 PM

Here is the z3 proof output.

erniecohen wrote Aug 28, 2015 at 12:01 PM

Here is a minimal .bpl that seems to lead to the contradiction:
const unique ^P: $ctype;
axiom $def_struct_type(^P, 1, false, false);

procedure test();
implementation test()
    assume $function_entry($s);
    assume $can_use_all_frame_axioms($s);
    assert false;