Project

General

Profile

Bug #4687

qflra/uf/prop gives wrong result for claim 1 of /main-bench/Funfrog15_bench/s3.c

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

Status:
Closed
Priority:
Normal
Assignee:
Karine Even Mendoza
Start date:
07/03/2017
Due date:
% Done:

100%

Estimated time:

Description

./hifrog --claim 1 --unwind 1 ~/dev/hi-bench/main-bench/Funfrog15_bench/token.c --logic qflra

Hifrog gives VERIFICATION FAILED for claim 1 in logic qflra/uf/prop

the correct result of claim 1: VERIFICATION Successful

History

#1 Updated by Karine Even Mendoza about 7 years ago

  • Assignee set to Karine Even Mendoza
  • % Done changed from 0 to 100

globals issues

#2 Updated by Karine Even Mendoza about 7 years ago

  • Status changed from New to Resolved

#3 Updated by Karine Even Mendoza about 7 years ago

  • Status changed from Resolved to Closed

Seems to be ok now

Processing a deferred function: is_transmit9_triggered
Processing a deferred function: is_transmit10_triggered
Processing a deferred function: is_transmit11_triggered
Processing a deferred function: is_transmit12_triggered
Processing a deferred function: is_transmit13_triggered
SYMEX TIME: 2.405
All SSA steps: 11336
Ignored SSA steps after slice: 6530
SLICER TIME: 0.014
; 0 | 0 0 | 3.200 s | 122.168 MB
; 210 | 56 56 | 9.420 s | 124.855 MB
; 331 | 145 145 | 11.260 s | 124.984 MB
CONVERSION TIME: 0.108
SOLVER TIME: 9.181
RESULT: UNSAT - it holds!
Start generating interpolants...
INTERPOLATION TIME: 3.907

VERIFICATION SUCCESSFUL
ASSERTION HOLDInitial unwinding bound: 1
Total number of steps: 1
TOTAL TIME FOR CHECKING THIS CLAIM: 15.644
#X: Done.
karinek@karinek-VirtualBox:~/workspace/tools/hi-bench$ ./../hifrog_theory_ref/hifrog/trunk/cprover/src/funfrog/hifrog --claim 1 --unwind 1 main-bench/Funfrog15_bench/token.c --logic qflra

Also available in: Atom PDF