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 __arr32__lu[36] : w32 -> w8 = symbolic
(query [(Eq false
(Eq 0
N0:(ReadLSB w32 0 __arr32__lu)))
(Eq false
(Eq 0
N1:(ReadLSB w32 4 __arr32__lu)))
(Eq false
(Eq 0
(ReadLSB w32 8 __arr32__lu)))
(Eq false
(Eq 0
N2:(ReadLSB w32 12 __arr32__lu)))
(Eq false
(Eq 0
N3:(ReadLSB w32 16 __arr32__lu)))
(Eq false
(Eq 0
(ReadLSB w32 20 __arr32__lu)))
(Eq false
(Eq 0
N4:(ReadLSB w32 24 __arr32__lu)))
(Eq false
(Eq 0
N5:(ReadLSB w32 28 __arr32__lu)))
(Eq false
(Eq 0
(ReadLSB w32 32 __arr32__lu)))
(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 __arr32__lu[36] : w32 -> w8 = symbolic
(query [(Eq false
(Eq 0
N0:(ReadLSB w32 0 __arr32__lu)))
(Eq false
(Eq 0
N1:(ReadLSB w32 4 __arr32__lu)))
(Eq false
(Eq 0
(ReadLSB w32 8 __arr32__lu)))
(Eq false
(Eq 0
N2:(ReadLSB w32 12 __arr32__lu)))
(Eq false
(Eq 0
N3:(ReadLSB w32 16 __arr32__lu)))
(Eq false
(Eq 0
(ReadLSB w32 20 __arr32__lu)))
(Eq false
(Eq 0
N4:(ReadLSB w32 24 __arr32__lu)))
(Eq false
(Eq 0
N5:(ReadLSB w32 28 __arr32__lu)))
(Eq false
(Eq 0
(ReadLSB w32 32 __arr32__lu)))
(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 __arr32__lu[36] : w32 -> w8 = symbolic
(query [(Eq false
(Eq 0
N0:(ReadLSB w32 0 __arr32__lu)))
(Eq false
(Eq 0
N1:(ReadLSB w32 4 __arr32__lu)))
(Eq false
(Eq 0
(ReadLSB w32 8 __arr32__lu)))
(Eq false
(Eq 0
N2:(ReadLSB w32 12 __arr32__lu)))
(Eq false
(Eq 0
N3:(ReadLSB w32 16 __arr32__lu)))
(Eq false
(Eq 0
(ReadLSB w32 20 __arr32__lu)))
(Eq false
(Eq 0
N4:(ReadLSB w32 24 __arr32__lu)))
(Eq false
(Eq 0
N5:(ReadLSB w32 28 __arr32__lu)))
(Eq false
(Eq 0
(ReadLSB w32 32 __arr32__lu)))
(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))"