Bug #3488
openSIGSEGV in LRASolver
100%
Description
The following stack trace appears when running the example rec.c (attached)
Program received signal SIGSEGV, Segmentation fault.
0x00007ffff7a54750 in LAVar::U (this=0x0) at LAVar.h:284
284 assert( all_bounds[u_bound].delta );
(gdb) bt
#0 0x00007ffff7a54750 in LAVar::U (this=0x0) at LAVar.h:284
#1 0x00007ffff7a66411 in LAVar::isModelOutOfBounds (this=0x0) at LAVar.h:184
#2 0x00007ffff7a59947 in LRASolver::check (this=0x1af86d0, complete=false) at LRASolver.C:458
#3 0x00007ffff7a4a33a in TSolverHandler::check (this=0x1e07420, complete=false) at TSolverHandler.C:80
#4 0x00007ffff7a43652 in THandler::check (this=0x207d0f0, complete=false) at THandler.C:132
#5 0x00007ffff7abd382 in CoreSMTSolver::checkTheory (this=0x1aac0e0, complete=false) at Theory.C:91
#6 0x00007ffff7ab1138 in CoreSMTSolver::search (this=0x1aac0e0, nof_conflicts=100, nof_learnts=29) at CoreSMTSolver.C:1863
#7 0x00007ffff7ab325b in CoreSMTSolver::solve_ (this=0x1aac0e0, max_conflicts=0) at CoreSMTSolver.C:2424
#8 0x00007ffff7aa3717 in SimpSMTSolver::solve_ (this=0x1aac0e0, do_simp=false, turn_off_simp=true) at SimpSMTSolver.C:185
#9 0x00007ffff7b062d2 in SimpSMTSolver::solve (this=0x1aac0e0, assumps=..., do_simp=false, turn_off_simp=true) at ../../src/smtsolvers/SimpSMTSolver.h:263
#10 0x00007ffff7b03553 in Cnfizer::solve (this=0x170ccc8, en_frames=...) at Cnfizer.C:88
#11 0x00007ffff7ad1430 in MainSolver::solve (this=0x170cc90) at MainSolver.C:1090
#12 0x00007ffff7ad127e in MainSolver::check (this=0x170cc90) at MainSolver.C:1069
#13 0x0000000000589ccc in smtcheck_opensmt2t::solve (this=0xeab100) at solvers/smtcheck_opensmt2.cpp:845
#14 0x00000000004625f0 in prop_assertion_sumt::is_satisfiable (this=0x7fffffffc2f0, decider=...) at prop_assertion_sum.cpp:130
#15 0x0000000000462451 in prop_assertion_sumt::assertion_holds (this=0x7fffffffc2f0, assertion=..., ns=..., decider=..., interpolator=...) at prop_assertion_sum.cpp:51
#16 0x00000000004771b4 in summarizing_checkert::assertion_holds (this=0x7fffffffd700, assertion=..., store_summaries_with_assertion=false) at summarizing_checker.cpp:127
#17 0x0000000000455fbe in check_claims (ns=..., leaping_program=..., goto_functions=..., claim_map=..., claim_numbers=..., options=..., _message_handler=..., claim_nr=0) at check_claims.cpp:211
#18 0x000000000044fbff in funfrog_parseoptionst::check_function_summarization (this=0x7fffffffe2b0, ns=..., goto_functions=...) at parseoptions.cpp:562
#19 0x000000000044edeb in funfrog_parseoptionst::doit (this=0x7fffffffe2b0) at parseoptions.cpp:312
#20 0x00000000007c05dc in parseoptions_baset::main (this=0x7fffffffe2b0) at parseoptions.cpp:104
#21 0x000000000048079f in main (argc=2, argv=0x7fffffffea48) at main.cpp:36
Files