diff --git a/regression/cbmc-concurrency/graphml_witness1/main.c b/regression/cbmc-concurrency/graphml_witness1/main.c new file mode 100644 index 00000000000..368332795a8 --- /dev/null +++ b/regression/cbmc-concurrency/graphml_witness1/main.c @@ -0,0 +1,8 @@ +int global; + +int main() +{ + __CPROVER_ASYNC_1: global=1; + global=2; + assert(global==2); // to fail +} diff --git a/regression/cbmc-concurrency/graphml_witness1/test.desc b/regression/cbmc-concurrency/graphml_witness1/test.desc new file mode 100644 index 00000000000..4bc835a150c --- /dev/null +++ b/regression/cbmc-concurrency/graphml_witness1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--graphml-witness - +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ + + +-- +^warning: ignoring diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 4f4f6f56741..9c2c8d2f51c 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -141,7 +141,7 @@ static bool filter_out( goto_tracet::stepst::const_iterator &it) { if(it->hidden && - (!it->is_assignment() || + (!it->pc->is_assign() || to_code_assign(it->pc->code).rhs().id()!=ID_side_effect || to_code_assign(it->pc->code).rhs().get(ID_statement)!=ID_nondet)) return true;