[klee-dev] Assertion klee: Solver.cpp:1103: MINISAT::PropagatedFrom MINISAT::Solver::propagate(bool): Assertion `c[1] == false_lit' failed.

Daniel Liew daniel.liew at imperial.ac.uk
Fri Apr 25 15:04:20 BST 2014 

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 <t.kuchta12 at imperial.ac.uk> 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 <kirill.sc at gmail.com>
> Date: Friday, 25 April 2014 14:02
> To: klee-dev <klee-dev at imperial.ac.uk>
> 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

More information about the klee-dev mailing list