Project

General

Profile

Bug #5306

inconsistency with CBMC is s3.c

Added by Sepideh Asadi about 2 years ago. Updated about 2 years ago.

Status:
Feedback
Priority:
Normal
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 about 2 years ago

--claim 131 s3.c

--claim 115

--claim 109

-claim 51

44

#2 Updated by Karine Even Mendoza about 2 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 about 2 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 :-)

Also available in: Atom PDF