Bug #7278
crash in VTT (1)
0%
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 almost 6 years 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 almost 6 years 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 almost 6 years ago
- Assignee set to Martin Blicha
#4 Updated by Martin Blicha almost 6 years 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.