[klee-dev] Assertion klee: Solver.cpp:1103: MINISAT::PropagatedFrom MINISAT::Solver::propagate(bool): Assertion `c[1] == false_lit' failed.
Kuchta, Tomasz
t.kuchta12 at imperial.ac.uk
Fri Apr 25 14:56:24 BST 2014
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<mailto:kirill.sc at gmail.com>>
Date: Friday, 25 April 2014 14:02
To: klee-dev <klee-dev at imperial.ac.uk<mailto: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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 13524 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20140425/f185407c/attachment.bin>
More information about the klee-dev
mailing list