Project

General

Profile

Actions
Copy link

Bug #5306

open

inconsistency with CBMC is s3.c

Added by Sepideh Asadi over 7 years ago. Updated over 7 years ago.

Status:
Feedback
Priority:
Normal
Assignee:
Antti Hyvärinen
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
Copy link
 #1

Updated by Sepideh Asadi over 7 years ago

--claim 131 s3.c

--claim 115

--claim 109

-claim 51

44

Actions
Copy link
 #2

Updated by Karine Even Mendoza over 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.

Actions
Copy link
 #3

Updated by Karine Even Mendoza over 7 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 :-)

Actions
Copy link

Also available in: Atom PDF