Actions
Bug #5306
openinconsistency 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
Actions
Added by Sepideh Asadi over 7 years ago. Updated over 7 years ago.
0%
Description
HiFRog: s3.c --theoref --bitwidth 32 --claim 29 SAT 1.48
CBMC: s3.c.c --claim 29 UNSAT 6.1
--claim 131 s3.c
--claim 115
--claim 109
-claim 51
44
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.
Classic one, just waiting for us to improve/add new support :-)