We tried two versions of STP (r940 and the latest) and KLEE gives us the message "BVTypeCheck: terms in atomic formulas must be of equal length" with both versions.
Below is the program we run using klee and the output. PROGRAM: #include <assert.h> #include <klee/klee.h> #define N 5 int avg (int x[N]) { int i; int ret; ret = 0; for (i = 0; i < N; i++) { ret = ret + x[i]; } return ret / N; } int main () { int x[N]; int temp; int ret; int ret2; int ret5; klee_make_symbolic(x, sizeof x, "x"); ret = avg(x); temp=x[0];x[0] = x[1]; x[1] = temp; ret2 = avg(x); temp=x[0]; int i; for(i =0 ; i<N-1; i++){ x[i] = x[i+1]; } x[N-1] = temp; ret5 = avg(x); if(ret != ret2 || ret !=ret5){ ERROR: goto ERROR; } return 1; } OUTPUT: KLEE: output directory is "XXXXXX" valuewidth of lhs of EQ: 32 valuewidth of rhs of EQ: 64 indexwidth of lhs of EQ: 0 indexwidth of rhs of EQ: 0 Fatal Error: BVTypeCheck: terms in atomic formulas must be of equal length 338:(EQ 142:0x00000002 336:0x000000000000003F) 0 error: STP Error: BVTypeCheck: terms in atomic formulas must be of equal length 0 klee 0x0000000000d9cb7f 1 klee 0x0000000000d9d089 2 libpthread.so.0 0x00007f0ac3162bd0 3 libc.so.6 0x00007f0ac239f037 gsignal + 55 4 libc.so.6 0x00007f0ac23a2698 abort + 328 5 klee 0x000000000062cbc9 6 klee 0x0000000000dcebcf BEEV::FatalError(char const*, BEEV::ASTNode const&, int) + 127 7 klee 0x0000000000dcf4f4 BEEV::BVTypeCheck(BEEV::ASTNode const&) + 1940 8 klee 0x0000000000db37a6 vc_iteExpr + 54 9 klee 0x0000000000632731 klee::STPBuilder::bvVarRightShift(klee::ExprHandle, klee::ExprHandle) + 225 10 klee 0x000000000063380c klee::STPBuilder::constructSDivByConstant(klee::ExprHandle, unsigned int, unsigned long) + 428 11 klee 0x00000000006365d1 klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*) + 7649 12 klee 0x0000000000633f13 klee::STPBuilder::construct(klee::ref<klee::Expr>, int*) + 323 13 klee 0x0000000000634c72 klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*) + 1154 14 klee 0x0000000000633f13 klee::STPBuilder::construct(klee::ref<klee::Expr>, int*) + 323 15 klee 0x0000000000630393 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&) + 387 16 klee 0x000000000061bd15 CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) + 245 17 klee 0x000000000061cf6b CexCachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 843 18 klee 0x000000000061a815 CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 149 19 klee 0x000000000062956b IndependentSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 315 20 klee 0x00000000005f7eee klee::TimingSolver::evaluate(klee::ExecutionState const&, klee::ref<klee::Expr>, klee::Solver::Validity&) + 366 21 klee 0x00000000005caaa2 klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) + 226 22 klee 0x00000000005d6ae3 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 9123 23 klee 0x00000000005d96d6 klee::Executor::run(klee::ExecutionState&) + 1798 24 klee 0x00000000005d9fdd klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1805 25 klee 0x00000000005b5c1c main + 6956 26 libc.so.6 0x00007f0ac2389ea5 __libc_start_main + 245 27 klee 0x00000000005bed31 Aborted (core dumped) _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev