Error when trying to compute real solutions

[Himeshi]

Ran the lu.bc file, (attached as text here) with the following arguments,

klee --write-kqueries --precision -compute-real-solution lu.bc

The execution crashed with the following error,

`KLEE: output directory is "/home/himeshi/Projects/workspace/LUScimark/klee-out-5" KLEE: Using Z3 solver backend KLEE: Using Z3 for reasoning about error expressions and/or path condition WARNING: this target does not support the llvm.stacksave intrinsic. KLEE: WARNING: unable to compute initial values (invalid constraints?)! array arr32lu[36] : w32 -> w8 = symbolic (query [(Eq false (Eq 0 N0:(ReadLSB w32 0 arr32lu))) (Eq false (Eq 0 N1:(ReadLSB w32 4 arr32lu))) (Eq false (Eq 0 (ReadLSB w32 8 arr32lu))) (Eq false (Eq 0 N2:(ReadLSB w32 12 arr32lu))) (Eq false (Eq 0 N3:(ReadLSB w32 16 arr32lu))) (Eq false (Eq 0 (ReadLSB w32 20 arr32lu))) (Eq false (Eq 0 N4:(ReadLSB w32 24 arr32lu))) (Eq false (Eq 0 N5:(ReadLSB w32 28 arr32lu))) (Eq false (Eq 0 (ReadLSB w32 32 arr32lu))) (Sle 0 N0) (Sle 0 N2) (Eq false (Slt N0 N2)) (Eq false (Sle 0 N4)) (Eq false (Slt N0 (Sub w32 0 N4))) (Eq false (Sle 0 N6:(Sub w32 N5 (Mul w32 (Mul w32 N4 N7:(SDiv w32 1 N0)) N1)))) (Eq false (Slt 0 (Sub w32 0 N6))) (Eq 0 (Sub w32 N3 (Mul w32 (Mul w32 N2 N7) N1)))] false) KLEE: WARNING: unable to compute initial values (invalid constraints?)! array arr32lu[36] : w32 -> w8 = symbolic (query [(Eq false (Eq 0 N0:(ReadLSB w32 0 arr32lu))) (Eq false (Eq 0 N1:(ReadLSB w32 4 arr32lu))) (Eq false (Eq 0 (ReadLSB w32 8 arr32lu))) (Eq false (Eq 0 N2:(ReadLSB w32 12 arr32lu))) (Eq false (Eq 0 N3:(ReadLSB w32 16 arr32lu))) (Eq false (Eq 0 (ReadLSB w32 20 arr32lu))) (Eq false (Eq 0 N4:(ReadLSB w32 24 arr32lu))) (Eq false (Eq 0 N5:(ReadLSB w32 28 arr32lu))) (Eq false (Eq 0 (ReadLSB w32 32 arr32lu))) (Sle 0 N0) (Eq false (Sle 0 N2)) (Eq false (Slt N0 (Sub w32 0 N2))) (Eq false (Sle 0 N4)) (Eq false (Slt N0 (Sub w32 0 N4))) (Eq false (Sle 0 N6:(Sub w32 N5 (Mul w32 (Mul w32 N4 N7:(SDiv w32 1 N0)) N1)))) (Eq false (Slt 0 (Sub w32 0 N6))) (Eq 0 (Sub w32 N3 (Mul w32 (Mul w32 N2 N7) N1)))] false) KLEE: WARNING: unable to compute initial values (invalid constraints?)! array arr32lu[36] : w32 -> w8 = symbolic (query [(Eq false (Eq 0 N0:(ReadLSB w32 0 arr32lu))) (Eq false (Eq 0 N1:(ReadLSB w32 4 arr32lu))) (Eq false (Eq 0 (ReadLSB w32 8 arr32lu))) (Eq false (Eq 0 N2:(ReadLSB w32 12 arr32lu))) (Eq false (Eq 0 N3:(ReadLSB w32 16 arr32lu))) (Eq false (Eq 0 (ReadLSB w32 20 arr32lu))) (Eq false (Eq 0 N4:(ReadLSB w32 24 arr32lu))) (Eq false (Eq 0 N5:(ReadLSB w32 28 arr32lu))) (Eq false (Eq 0 (ReadLSB w32 32 arr32lu))) (Eq false (Sle 0 N0)) (Sle 0 N2) (Eq false (Slt N6:(Sub w32 0 N0) N2)) (Sle 0 N4) (Eq false (Slt N6 N4)) (Eq false (Sle 0 N7:(Sub w32 N5 (Mul w32 (Mul w32 N4 N8:(SDiv w32 1 N0)) N1)))) (Eq false (Slt 0 (Sub w32 0 N7))) (Eq 0 (Sub w32 N3 (Mul w32 (Mul w32 N2 N8) N1)))] false) KLEE: WARNING: Unexpected solver failure. Reason is "(incomplete (theory arithmetic)),"

0 klee 0x000000000130cab2 llvm::sys::PrintStackTrace(_IO_FILE) + 53 1 klee 0x000000000130cd42 2 klee 0x000000000130c70b 3 libpthread.so.0 0x00007f4bf6c63390 4 libc.so.6 0x00007f4bf442b428 gsignal + 56 5 libc.so.6 0x00007f4bf442d02a abort + 362 6 klee 0x0000000000880069 klee::Z3ErrorSolverImpl::handleSolverResponse(_Z3_solver, Z3_lbool, std::vector<klee::Array const, std::allocator<klee::Array const> > const, std::vector<std::vector<unsigned char, std::allocator >, std::allocator<std::vector<unsigned char, std::allocator > > >, bool&) + 1721 7 klee 0x0000000000880401 klee::Z3ErrorSolverImpl::internalRunSolver(klee::Query const&, std::vector<klee::Array const, std::allocator<klee::Array const> > const, std::vector<std::vector<unsigned char, std::allocator >, std::allocator<std::vector<unsigned char, std::allocator > > >, bool&) + 817 8 klee 0x000000000087d123 klee::Solver::getInitialValues(klee::Query const&, std::vector<klee::Array const, std::allocator<klee::Array const> > const&, std::vector<std::vector<unsigned char, std::allocator >, std::allocator<std::vector<unsigned char, std::allocator > > >&) + 35 9 klee 0x00000000007f471b klee::Executor::getRealSymbolicSolution(klee::ExecutionState const&, std::vector<std::pair<std::cxx11::basic_string<char, std::char_traits, std::allocator >, double>, std::allocator<std::pair<std::cxx11::basic_string<char, std::char_traits, std::allocator >, double> > >&) + 347 10 klee 0x00000000007e1267 11 klee 0x00000000007f5156 klee::Executor::terminateStateOnExit(klee::ExecutionState&) + 38 12 klee 0x00000000008059db klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction) + 18059 13 klee 0x0000000000809a9c klee::Executor::run(klee::ExecutionState&) + 1676 14 klee 0x000000000080a2e0 klee::Executor::runFunctionAsMain(llvm::Function, int, char, char) + 1600 15 klee 0x00000000007d5dcc main + 11836 16 libc.so.6 0x00007f4bf4416830 __libc_start_main + 240 17 klee 0x00000000007dd719 _start + 41 Aborted (core dumped)`

[Himeshi]

lu.bc.zip

[domainexpert]

@Himeshi This means there is a nonlinear constraint in the expression which cannot be solved, from this warning:

KLEE: WARNING: Unexpected solver failure. Reason is "(incomplete (theory arithmetic))"