Bug #5306
inconsistency with CBMC is s3.c
Start date:
15/06/2017
Due date:
% Done:
0%
Estimated time:
Description
HiFRog: s3.c --theoref --bitwidth 32 --claim 29 SAT 1.48
CBMC: s3.c.c --claim 29 UNSAT 6.1
History
#1 Updated by Sepideh Asadi almost 7 years ago
--claim 131 s3.c
--claim 115
--claim 109
-claim 51
44
#2 Updated by Karine Even Mendoza almost 7 years ago
- Priority changed from Normal to High
1. Add new supports for more operators in OpenSMT side (so we can BB these), as well as in HiFrog side.
2. New Heuristics that do not need all operators to find SAT results.
#3 Updated by Karine Even Mendoza over 6 years ago
- Status changed from New to Feedback
- Assignee set to Antti Hyvärinen
- Priority changed from High to Normal
Classic one, just waiting for us to improve/add new support :-)