Project

General

Profile

Bug #7278

crash in VTT (1)

Added by Sepideh Asadi over 1 year ago. Updated over 1 year ago.

Status:
Resolved
Priority:
High
Assignee:
Start date:
07/05/2018
Due date:
% Done:

0%

Estimated time:

Description

File: /cprover/regression/funfrog/VTT/P2P_Joints_TG3_e_num_4.c

how to run: ./hifrog --unwind 10 --sum-theoref

Error log:

Verification not successful, here is the last few lines: ...

Processing a deferred function: sqrt_
Processing a deferred function: sqrt_
SYMEX TIME: 0.708
All SSA steps: 672
Ignored SSA steps after slice: 214
SLICER TIME: 0.007
; uf_solver query time so far: 0.000000
; 0 | 0 0 | 84.680 s | 871.938 MB

---trying to locally refine the summary in UF---

---EUF was not enough, lets change the encoding to LRA---

; Warning: disabling SATElite preprocessing to track proof
hifrog: ~/cprover/src/funfrog/solvers/smtcheck_opensmt2.cpp:1090: PTRef smtcheck_opensmt2t::substitute(smt_itpt&, const std::vector<symbol_exprt>&): Assertion `symbols.size() == static_cast<std::size_t>(args.size())' failed.
Command terminated by signal 6
time 85.37

History

#1 Updated by Karine Even Mendoza over 1 year ago

Happens in: PTRef smtcheck_opensmt2t::substitute(smt_itpt & itp, const std::vector<symbol_exprt> & symbols)

no args to substitute, I assume that due to some error we send an empty vector.

#2 Updated by Karine Even Mendoza over 1 year ago

args: 4 vs. symbols: 5

symbol sqrt_::a
symbol hifrog::fun_start
symbol hifrog::fun_end
symbol hifrog::?err
symbol sqrt_::#return_value
arg sqrt_::a
arg hifrog::fun_start
arg hifrog::fun_end
arg sqrt_::#return_value

hifrog: /home/karinek/workspace/sum_theoref/hifrog/trunk/cprover/src/funfrog/solvers/smtcheck_opensmt2.cpp:1098: PTRef smtcheck_opensmt2t::substitute(smt_itpt&, const std::vector<symbol_exprt>&): Assertion `symbols.size() == static_cast<std::size_t>(args.size())' failed.
Aborted (core dumped)

#3 Updated by Karine Even Mendoza over 1 year ago

  • Assignee set to Martin Blicha

#4 Updated by Martin Blicha over 1 year ago

  • Status changed from New to Resolved

There was a problem when moving from UF to LRA level. When summaries from previous iteration were present even for functions that now had the assertion in its call tree, this method was marked to use that summary, which is incorrect. We do not summarize functions with assertion in its call tree.
See commit 707ab6bc.

Also available in: Atom PDF