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

Fri Apr 25 14:02:37 BST 2014

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 --------------
HTML attachment scrubbed and removed