Command exited with non-zero status 10 341.41user 5.19system 5:48.17elapsed 99%CPU (0avgtext+0avgdata 58080maxresident)k 0inputs+9536outputs (0major+2020871minor)pagefaults 0swaps 0 Generating GOTO Program Pointer Analysis Adding Pointer Checks Starting Bounded Model Checking Unwinding loop 1 iteration 1 Unwinding loop 1 iteration 2 Unwinding loop 1 iteration 3 Unwinding loop 1 iteration 4 Unwinding loop 1 iteration 5 Unwinding loop 1 iteration 6 Unwinding loop 1 iteration 7 Unwinding loop 1 iteration 8 Unwinding loop 1 iteration 9 Unwinding loop 1 iteration 10 Unwinding loop 1 iteration 11 Unwinding loop 1 iteration 12 Unwinding loop 1 iteration 13 Unwinding loop 1 iteration 14 Unwinding loop 1 iteration 15 Unwinding loop 1 iteration 16 Unwinding loop 1 iteration 17 Unwinding loop 1 iteration 18 Unwinding loop 1 iteration 19 Unwinding loop 1 iteration 20 Unwinding loop 1 iteration 21 Unwinding loop 1 iteration 22 Unwinding loop 1 iteration 23 Unwinding loop 1 iteration 24 Unwinding loop 1 iteration 25 Unwinding loop 1 iteration 26 Unwinding loop 1 iteration 27 Unwinding loop 1 iteration 28 Unwinding loop 1 iteration 29 Unwinding loop 1 iteration 30 Unwinding loop 1 iteration 31 Unwinding loop 1 iteration 32 Unwinding loop 1 iteration 33 Unwinding loop 1 iteration 34 Unwinding loop 1 iteration 35 Unwinding loop 1 iteration 36 Unwinding loop 1 iteration 37 Unwinding loop 1 iteration 38 Unwinding loop 1 iteration 39 Unwinding loop 1 iteration 40 Unwinding loop 1 iteration 41 Unwinding loop 1 iteration 42 Unwinding loop 1 iteration 43 Unwinding loop 1 iteration 44 Unwinding loop 1 iteration 45 Unwinding loop 1 iteration 46 Unwinding loop 1 iteration 47 Unwinding loop 1 iteration 48 Unwinding loop 1 iteration 49 Unwinding loop 1 iteration 50 Unwinding loop 1 iteration 51 Unwinding loop 1 iteration 52 Unwinding loop 1 iteration 53 Unwinding loop 1 iteration 54 Unwinding loop 1 iteration 55 Unwinding loop 1 iteration 56 size of program expression: 402 assignments Generated 3 claims, 3 remaining Passing problem to MiniSAT Passing to decision procedure Running MiniSAT Solving with MiniSAT 43708 variables, 44492 clauses SAT checker: negated claim is SATISFIABLE, i.e., does not hold Building error trace Counterexample: Violated property: file /home/mdbekkouche/These/Benchmarks_MCS-IIS/Programs_Benchmarks_MCS-IIS_BugAssist/ProgrammesWhile/Programs/WithoutArray/Sum/Versions/SumV50.c line 11 assertion s == n * (n + 1) / 2 < 1 > Potential BUG @ :/home/mdbekkouche/These/Benchmarks_MCS-IIS/Programs_Benchmarks_MCS-IIS_BugAssist/ProgrammesWhile/Programs/WithoutArray/Sum/Versions/SumV50.c:9 < 7 > Potential BUG @ :/home/mdbekkouche/These/Benchmarks_MCS-IIS/Programs_Benchmarks_MCS-IIS_BugAssist/ProgrammesWhile/Programs/WithoutArray/Sum/Versions/SumV50.c:11 < 57 > Potential BUG @ :/home/mdbekkouche/These/Benchmarks_MCS-IIS/Programs_Benchmarks_MCS-IIS_BugAssist/ProgrammesWhile/Programs/WithoutArray/Sum/Versions/SumV50.c:7 < 112 > Potential BUG @ :/home/mdbekkouche/These/Benchmarks_MCS-IIS/Programs_Benchmarks_MCS-IIS_BugAssist/ProgrammesWhile/Programs/WithoutArray/Sum/Versions/SumV50.c:8 BUG Assist: No More suspects: VERIFICATION FAILED