Project

General

Profile

Bug #4686

qflra/uf/prop gives wrong result for /main-bench/Funfrog15_bench/token.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 all the logic qflra/uf/prop

the correct result is 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 In Progress
  • % Done changed from 100 to 70

General problem in prop due to changes in cprover version. LRA works fine.

Processing a deferred function: is_transmit11_triggered
Processing a deferred function: is_transmit12_triggered
Processing a deferred function: is_transmit13_triggered
SYMEX TIME: 2.142
All SSA steps: 11336
Ignored SSA steps after slice: 6530
SLICER TIME: 0.014
Trivial partition (terms size = 1): 224
CONVERSION TIME: 4.381
Post-processing
Solving with OpenSMT2 (QF_BOOL)
; 0 | 0 0 | 10.044 s | 267.953 MB
RESULT
SOLVER TIME: 3.545
hifrog: solvers/prop_itp.cpp:366: void prop_itpt::generalize(const prop_conv_solvert&, const std::vector<symbol_exprt>&): Assertion `renaming[idx] != (0x7fffffff * 2U + 1U)' failed.
Aborted (core dumped)
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 prop

#4 Updated by Karine Even Mendoza about 7 years ago

  • Status changed from In Progress to Resolved
  • % Done changed from 70 to 100

After (partially) fixed the bug:

Start generating interpolants...INTERPOLATION TIME: 1.597
; -------------------------
; STATISTICS FOR SAT SOLVER
; -------------------------
; Restarts.................: 1
; Conflicts................: 4
; Decisions................: 11
; Propagations.............: 17830
; Conflict literals........: 3
; T-Lemmata learnt.........: 0
; T-Lemmata perm learnt....: 0
; Conflicts learnt.........: 4
; T-conflicts learnt.......: 0
; Average learnts size.....: 0
; Top level literals.......: 13549
; Search time..............: 0 s
; TSolvers time............: 0 s
; Init clauses.............: 99002
; Variables................: 41499
; -------------------------
; STATISTICS FOR EUF SOLVER
; -------------------------
; Satisfiable calls........: 0
; Unsatisfiable calls......: 0
; egraph time..............: 0 s
; backtrack time...........: 0 s
; explain time.............: 0 s
; -------------------------
; STATISTICS FOR LOGICS
; -------------------------
; Substitutions............: 0

VERIFICATION SUCCESSFUL
ASSERTION HOLDInitial unwinding bound: 1
Total number of steps: 1
TOTAL TIME FOR CHECKING THIS CLAIM: 16.106
#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 prop

#5 Updated by Karine Even Mendoza about 7 years ago

  • Status changed from Resolved to Closed

Also available in: Atom PDF