/* ==================================
   C program
   ==================================*/
extern int nd (void);
extern void __CRAB_assert(int);

int x = 5;
int y = 3;

int a[10];

int main ()
{
  int i;
  int *p =&x;
  *p= *p + 1;
  for (i=0;i<10;i++)
  {
    if (nd ())
      a[i] =y;
    else 
      a[i] =x;
  }
  y++;
  int res = a[i-1];

  __CRAB_assert(res >= 0 && res <= 6);
  return res;
}

/* ===================================
   LLVM bitecode
   ===================================*/

; ModuleID = '/var/folders/rd/wyr_48nj7qj5jy6nx62ftjlm0000gq/T/crabllvm-YApt7b/test-arr-2.pp.bc'
target datalayout = "e-m:o-p:32:32-f64:32:64-f80:128-n8:16:32-S128"
target triple = "i386-apple-macosx10.11.0"

@x = internal global i32 5, align 4
@a = internal unnamed_addr global [10 x i32] zeroinitializer, align 4

; Function Attrs: nounwind ssp
define i32 @main() #0 {
_call:
  call void @verifier.zero_initializer.1(i32* @x)
  call void @verifier.zero_initializer.2([10 x i32]* @a)
  %_2 = load i32* @x, align 4
  %_store = add nsw i32 %_2, 1
  store i32 %_store, i32* @x, align 4
  br label %_i.0

_i.0:                                             ; preds = %_14, %_call
  %i.0 = phi i32 [ 0, %_call ], [ %_br4, %_14 ]
  %_br = icmp slt i32 %i.0, 10
  br i1 %_br, label %_6, label %PHILowerICmp

_6:                                               ; preds = %_i.0
  %_7 = call i32 @nd() #2
  %_br1 = icmp eq i32 %_7, 0
  br i1 %_br1, label %_11, label %_9

_9:                                               ; preds = %_6
  %_store2 = getelementptr inbounds [10 x i32]* @a, i32 0, i32 %i.0
  store i32 3, i32* %_store2, align 4
  br label %_14

_11:                                              ; preds = %_6
  %_12 = load i32* @x, align 4
  %_store3 = getelementptr inbounds [10 x i32]* @a, i32 0, i32 %i.0
  store i32 %_12, i32* %_store3, align 4
  br label %_14

_14:                                              ; preds = %_11, %_9
  %_br4 = add nsw i32 %i.0, 1
  br label %_i.0

PHILowerICmp:                                     ; preds = %_i.0
  %i.0.lcssa = phi i32 [ %i.0, %_i.0 ]
  %_16 = add nsw i32 %i.0.lcssa, -1
  %_17 = getelementptr inbounds [10 x i32]* @a, i32 0, i32 %_16
  %_check_SGE_0 = load i32* %_17, align 4
  %check_SGE_0 = icmp sle i32 0, %_check_SGE_0
  %_19 = icmp slt i32 %_check_SGE_0, 7
  %_20 = select i1 %check_SGE_0, i1 %_19, i1 true
  %_call5 = zext i1 %_20 to i32
  call void @__CRAB_assert(i32 %_call5) #2
  ret i32 %_check_SGE_0
}

declare i32 @nd() #1

declare void @__CRAB_assert(i32) #1

declare void @verifier.zero_initializer.1(i32*)

declare void @verifier.zero_initializer.2([10 x i32]*)

attributes #0 = { nounwind ssp "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "stack-protector-buffer-size"="8" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #1 = { "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "stack-protector-buffer-size"="8" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #2 = { nounwind }

!llvm.module.flags = !{!0}
!llvm.ident = !{!1}

!0 = !{i32 1, !"PIC Level", i32 2}
!1 = !{!"clang version 3.6.0 (tags/RELEASE_360/final)"}

/* =====================================
   side-effect-free translation from LLVM bitcode
   =====================================*/

_check_SGE_0:int declare main()
_call:
  assume (forall l in [0,0] % 4 :: @V_1[l]=0);
  assume (forall l in [0,36] % 4 :: @V_2[l]=0);
  _2 = array_read(@V_1,x);
  _store = _2+1;
  array_write(@V_1,x,_store);
  i.0 = 0;
--> [_i.0;]
_i.0:
--> [__@bb_1;__@bb_2;]
__@bb_1:
  assume (i.0 <= 9);
--> [_6;]
_6:
  _7 =* ;
--> [__@bb_3;__@bb_4;]
__@bb_3:
  assume (_7 = 0);
--> [_11;]
_11:
  _12 = array_read(@V_1,x);
  _store3 = a + 4*i.0;
  array_write(@V_2,_store3,_12);
--> [_14;]
_14:
  _br4 = i.0+1;
  i.0 = _br4;
--> [_i.0;]
__@bb_4:
  assume (_7 != 0);
--> [_9;]
_9:
  _store2 = a + 4*i.0;
  array_write(@V_2,_store2,3);
--> [_14;]
__@bb_2:
  assume (-i.0 <= -10);
  i.0.lcssa = i.0;
--> [PHILowerICmp;]
PHILowerICmp:
  _16 = i.0.lcssa+-1;
  _17 = a + 4*_16;
  _check_SGE_0 = array_read(@V_2,_17);
  check_SGE_0 = (-_check_SGE_0 <= 0);
  _19 = (_check_SGE_0 <= 6);
  @V_20 = true ;
  _20 = ite(check_SGE_0,_19,@V_20);
  zext _20:1 to _call5:32;
  assert (-_call5 <= -1);
  return _check_SGE_0;
--> []