Command exited with non-zero status 10 3.74user 0.17system 0:04.34elapsed 90%CPU (0avgtext+0avgdata 11784maxresident)k 0inputs+1456outputs (0major+57052minor)pagefaults 0swaps ng Checking SquareRootV2 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 size of program expression: 95 assignments Generated 2 claims, 2 remaining Passing problem to MiniSAT Passing to decision procedure Running MiniSAT Solving with MiniSAT 8701 variables, 4091 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/SquareRoot/Versions/SquareRootV2.c line 14 assertion res * res <= val && (res + 1) * (res + 1) > val < 1 > Potential BUG @ :/home/mdbekkouche/These/Benchmarks_MCS-IIS/Programs_Benchmarks_MCS-IIS_BugAssist/ProgrammesWhile/Programs/WithoutArray/SquareRoot/Versions/SquareRootV2.c:10 < 2 > Potential BUG @ :/home/mdbekkouche/These/Benchmarks_MCS-IIS/Programs_Benchmarks_MCS-IIS_BugAssist/ProgrammesWhile/Programs/WithoutArray/SquareRoot/Versions/SquareRootV2.c:11 < 7 > Potential BUG @ :/home/mdbekkouche/These/Benchmarks_MCS-IIS/Programs_Benchmarks_MCS-IIS_BugAssist/ProgrammesWhile/Programs/WithoutArray/SquareRoot/Versions/SquareRootV2.c:13 < 11 > Potential BUG @ :/home/mdbekkouche/These/Benchmarks_MCS-IIS/Programs_Benchmarks_MCS-IIS_BugAssist/ProgrammesWhile/Programs/WithoutArray/SquareRoot/Versions/SquareRootV2.c:9 BUG Assist: No More suspects: VERIFICATION FAILED