The assertion is failing inside STP. I would probably try attaching to GDB, let it run so GDB can catch the assertion failure. Make sure you've built STP with debug symbols so you can get a useful backtrace.
On 25 April 2014 14:56, Kuchta, Tomasz <[email protected]> wrote: > Hi Kirill, > > I would check if you are not running out of memory and > try to do ulimit –s unlimited. > > Tomek > > From: Kirill Bogdanov <[email protected]> > Date: Friday, 25 April 2014 14:02 > To: klee-dev <[email protected]> > Subject: [klee-dev] Assertion klee: Solver.cpp:1103: MINISAT::PropagatedFrom > MINISAT::Solver::propagate(bool): Assertion `c[1] == false_lit' failed. > > Hello Everyone, > > I wonder if I can ask a question about KLEE FP here, I am getting an > assertion in Solver.cpp after 1 hour of klee-fp run and I am trying to > understand why. > > What is the meaning of this assertion? Am I doing something wrong? How can I > find which line in my code has triggered it? > > Any directions would be appreciated! > Thank you very much! > > $ clang -emit-llvm -c -g main.cpp > $ time klee -libc=uclibc main.o > KLEE: output directory = "klee-out-2" > KLEE: WARNING: undefined reference to function: _ZNSt8ios_base4InitC1Ev > KLEE: WARNING: undefined reference to function: _ZNSt8ios_base4InitD1Ev > KLEE: WARNING: undefined reference to function: _ZSt17__throw_bad_allocv > KLEE: WARNING: undefined reference to function: > _ZSt18_Rb_tree_decrementPKSt18_Rb_tree_node_base > KLEE: WARNING: undefined reference to function: > _ZSt18_Rb_tree_decrementPSt18_Rb_tree_node_base > KLEE: WARNING: undefined reference to function: > _ZSt18_Rb_tree_incrementPKSt18_Rb_tree_node_base > KLEE: WARNING: undefined reference to function: > _ZSt18_Rb_tree_incrementPSt18_Rb_tree_node_base > KLEE: WARNING: undefined reference to function: > _ZSt20__throw_out_of_rangePKc > KLEE: WARNING: undefined reference to function: > _ZSt28_Rb_tree_rebalance_for_erasePSt18_Rb_tree_node_baseRS_ > KLEE: WARNING: undefined reference to function: > _ZSt29_Rb_tree_insert_and_rebalancebPSt18_Rb_tree_node_baseS0_RS_ > KLEE: WARNING: undefined reference to function: _ZSt9terminatev > KLEE: WARNING: undefined reference to function: __cxa_begin_catch > KLEE: WARNING: undefined reference to function: __cxa_end_catch > KLEE: WARNING: undefined reference to function: __cxa_rethrow > KLEE: WARNING: undefined reference to function: __gxx_personality_v0 > KLEE: WARNING: undefined reference to function: __restore_rt > KLEE: WARNING: undefined reference to function: exp > KLEE: WARNING: undefined reference to function: fcntl > KLEE: WARNING: undefined reference to function: floor > KLEE: WARNING: undefined reference to function: klee_cos > KLEE: WARNING: undefined reference to function: klee_cosf > KLEE: WARNING: undefined reference to function: klee_sin > KLEE: WARNING: undefined reference to function: klee_sinf > KLEE: WARNING: undefined reference to function: klee_sqrt > KLEE: WARNING: undefined reference to function: klee_sqrtf > KLEE: WARNING: undefined reference to function: lseek64 > KLEE: WARNING: undefined reference to function: syscall > KLEE: WARNING: undefined reference to function: time > KLEE: WARNING: executable has module level assembly (ignoring) > KLEE: WARNING: calling external: _ZNSt8ios_base4InitC1Ev(139919863132416) > KLEE: WARNING: calling external: syscall(16, 0, 21505, 139919863148000) > KLEE: WARNING: calling __user_main with extra arguments. > KLEE: WARNING: calling external: time(0) > KLEE: WARNING: calling external: > _ZSt29_Rb_tree_insert_and_rebalancebPSt18_Rb_tree_node_baseS0_RS_(true, > 139919863156288, 139919863151184, 139919863151184) > KLEE: WARNING: calling external: exp(0) > KLEE: WARNING: calling external: > _ZSt18_Rb_tree_incrementPSt18_Rb_tree_node_base(139919863234656) > klee: Solver.cpp:1103: MINISAT::PropagatedFrom > MINISAT::Solver::propagate(bool): Assertion `c[1] == false_lit' failed. > 0 klee 0x0000000000e6bdcf > 1 klee 0x0000000000e6c2d9 > 2 libpthread.so.0 0x00007f41b29b7cb0 > 3 libc.so.6 0x00007f41b1c08425 gsignal + 53 > 4 libc.so.6 0x00007f41b1c0bb8b abort + 379 > 5 libc.so.6 0x00007f41b1c010ee > 6 libc.so.6 0x00007f41b1c01192 > 7 klee 0x0000000000ec6c85 MINISAT::Solver::propagate(bool) + > 1461 > 8 klee 0x0000000000ece364 MINISAT::Solver::search(int, int, > bool) + 196 > 9 klee 0x0000000000ecf009 > MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 1465 > 10 klee 0x0000000000ebfbe9 > BEEV::ToSAT::toSATandSolve(MINISAT::Solver&, BEEV::ClauseList&, bool, > BEEV::CNFMgr*&, bool, bool) + 3609 > 11 klee 0x0000000000ec021d > BEEV::ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver&, std::map<int, > BEEV::ClauseList*, BEEV::ltint, std::allocator<std::pair<int const, > BEEV::ClauseList*> > >*, BEEV::CNFMgr*&) + 125 > 12 klee 0x0000000000ec0dcc BEEV::ToSAT::CallSAT(MINISAT::Solver&, > BEEV::ASTNode const&) + 2956 > 13 klee 0x0000000000ebce2f > BEEV::AbsRefine_CounterExample::CallSAT_ResultCheck(MINISAT::Solver&, > BEEV::ASTNode const&, BEEV::ASTNode const&, BEEV::ToSATBase*) + 31 > 14 klee 0x0000000000eabab2 > BEEV::STP::TopLevelSTPAux(MINISAT::Solver&, BEEV::ASTNode const&, > BEEV::ASTNode const&) + 8050 > 15 klee 0x0000000000eacd8e BEEV::STP::TopLevelSTP(BEEV::ASTNode > const&, BEEV::ASTNode const&) + 238 > 16 klee 0x0000000000e85a4d vc_query + 157 > 17 klee 0x0000000000617fa5 > STPSolverImpl::computeInitialValues(klee::Query const&, > std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&, > std::vector<std::vector<unsigned char, std::allocator<unsigned char> >, > std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > > >>&, bool&) + 1477 > 18 klee 0x00000000006024ee > CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) + > 254 > 19 klee 0x0000000000603829 > CexCachingSolver::computeValidity(klee::Query const&, > klee::Solver::Validity&) + 1065 > 20 klee 0x0000000000600ff0 > CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) > + 144 > 21 klee 0x00000000006114cc > IndependentSolver::computeValidity(klee::Query const&, > klee::Solver::Validity&) + 348 > 22 klee 0x00000000005d59f2 > klee::TimingSolver::evaluate(klee::ExecutionState const&, > klee::ref<klee::Expr>, klee::Solver::Validity&) + 546 > 23 klee 0x000000000059ab3f > klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool, > int) + 303 > 24 klee 0x00000000005a3f02 > klee::Executor::executeInstruction(klee::ExecutionState&, > klee::KInstruction*) + 12706 > 25 klee 0x00000000005a71a2 > klee::Executor::run(klee::ExecutionState&) + 1906 > 26 klee 0x00000000005a7c1f > klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + > 1823 > 27 klee 0x000000000057ddf8 main + 5320 > 28 libc.so.6 0x00007f41b1bf376d __libc_start_main + 237 > 29 klee 0x000000000058df81 > Aborted (core dumped) > > real 100m21.991s > user 99m41.830s > sys 0m20.345s _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
