Project

General

Profile

Bug #4689

Caught exception: symex_assign_rec: unexpected assignment to union member

Added by Sepideh Asadi almost 6 years ago. Updated almost 6 years ago.

Status:
Closed
Priority:
Normal
Start date:
07/03/2017
Due date:
% Done:

100%

Estimated time:

Description

./hifrog --claim 7 ~/dev/hi-bench/main-bench/Funfrog15_bench/disk.c --logic prop/qflra/qfuf

History

#1 Updated by Sepideh Asadi almost 6 years ago

expected result for claim 7: successful verification

This problem is happening in almost all of disk.c
Caught exception: symex_assign_rec: unexpected assignment to union member

#2 Updated by Karine Even Mendoza almost 6 years ago

  • Assignee set to Karine Even Mendoza
  • % Done changed from 0 to 60

Cprover bug - follow up when upgrading the versions

#3 Updated by Karine Even Mendoza almost 6 years ago

  • % Done changed from 60 to 70

After cprover upgrade, all works but prop logic, need to check the assert there.

#4 Updated by Karine Even Mendoza almost 6 years ago

  • Status changed from New to In Progress

#5 Updated by Karine Even Mendoza almost 6 years ago

  • Status changed from In Progress to Closed
  • % Done changed from 70 to 100

fixed. added optimisations from cbmc

Also available in: Atom PDF