Bug #4689
Caught exception: symex_assign_rec: unexpected assignment to union member
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 about 7 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 about 7 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 about 7 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 about 7 years ago
- Status changed from New to In Progress
#5 Updated by Karine Even Mendoza almost 7 years ago
- Status changed from In Progress to Closed
- % Done changed from 70 to 100
fixed. added optimisations from cbmc