Project

General

Profile

Bug #4836

./hifrog ~/dev/hi-bench/main-bench/funfrog_regression/01_choice/main2_ok.c --claim 1

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

Status:
Closed
Priority:
Normal
Assignee:
Sepideh Asadi
Start date:
20/03/2017
Due date:
% Done:

100%

Estimated time:

Description

VERIFICATION FAILED

History

#1 Updated by Karine Even Mendoza about 7 years ago

  • Status changed from New to Feedback

Seem to be ok now - fails only to UF, but CUF is refining it. For prop and lra is SUCC with no refinement.
Is it the right result?

Trying to refine with CUF+BitBlast
(driven by iterative CE-analysis)

; Warning: disabling SATElite preprocessing to track proof
; 0 | 0 0 | 0.096 s | 153.051 MB
; 0 | 0 0 | 0.100 s | 153.051 MB
; 0 | 0 0 | 0.100 s | 153.051 MB
; 0 | 0 0 | 0.104 s | 153.051 MB
; Warning: disabling SATElite preprocessing to track proof
; Warning: disabling SATElite preprocessing to track proof
; Warning: disabling SATElite preprocessing to track proof
; Warning: disabling SATElite preprocessing to track proof
; Warning: disabling SATElite preprocessing to track proof
; Warning: disabling SATElite preprocessing to track proof
; Warning: disabling SATElite preprocessing to track proof
; Warning: disabling SATElite preprocessing to track proof
; Warning: disabling SATElite preprocessing to track proof
Weak statement encodings (9) found

Refinement successful
(9 / 13 expressions bit-blasted)
Command-line options to double-check: --theoref --custom 4,5,6,7,8,9,10,11,12,
ASSERTION HOLDS

VERIFICATION SUCCESSFUL
TOTAL TIME FOR CHECKING THIS CLAIM: 0.073

#2 Updated by Karine Even Mendoza about 7 years ago

  • Status changed from Feedback to Closed
  • % Done changed from 0 to 100

UF is buggy all over, the rest is working well now

Also available in: Atom PDF