add new test script

int __VERIFIER_assert(int);

int __VERIFIER_nondet_int(void);

int main() {

    int n = 5;

    int c = 2;

    for (int i = 0; i < 3 ; i++) {

        n += c;

    }

    __VERIFIER_assert(n == 11);

    return 0;

}

 No newline at end of file

; ModuleID = 'memory_loop3_t.c'

source_filename = "memory_loop3_t.c"

target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"

target triple = "x86_64-pc-linux-gnu"

; Function Attrs: noinline nounwind optnone uwtable

define dso_local i32 @main() #0 {

  %1 = alloca i32, align 4

  %2 = alloca i32, align 4

  %3 = alloca i32, align 4

  %4 = alloca i32, align 4

  store i32 0, i32* %1, align 4

  store i32 5, i32* %2, align 4

  store i32 2, i32* %3, align 4

  store i32 0, i32* %4, align 4

  br label %5

5:                                                ; preds = %12, %0

  %6 = load i32, i32* %4, align 4

  %7 = icmp slt i32 %6, 3

  br i1 %7, label %8, label %15

8:                                                ; preds = %5

  %9 = load i32, i32* %3, align 4

  %10 = load i32, i32* %2, align 4

  %11 = add nsw i32 %10, %9

  store i32 %11, i32* %2, align 4

  br label %12

12:                                               ; preds = %8

  %13 = load i32, i32* %4, align 4

  %14 = add nsw i32 %13, 1

  store i32 %14, i32* %4, align 4

  br label %5, !llvm.loop !6

15:                                               ; preds = %5

  %16 = load i32, i32* %2, align 4

  %17 = icmp eq i32 %16, 11

  %18 = zext i1 %17 to i32

  %19 = call i32 @__VERIFIER_assert(i32 noundef %18)

  ret i32 0

}

declare i32 @__VERIFIER_assert(i32 noundef) #1

attributes #0 = { noinline nounwind optnone uwtable "frame-pointer"="all" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }

attributes #1 = { "frame-pointer"="all" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }

!llvm.module.flags = !{!0, !1, !2, !3, !4}

!llvm.ident = !{!5}

!0 = !{i32 1, !"wchar_size", i32 4}

!1 = !{i32 7, !"PIC Level", i32 2}

!2 = !{i32 7, !"PIE Level", i32 2}

!3 = !{i32 7, !"uwtable", i32 1}

!4 = !{i32 7, !"frame-pointer", i32 2}

!5 = !{!"Ubuntu clang version 14.0.6"}

!6 = distinct !{!6, !7}

!7 = !{!"llvm.loop.mustprogress"}