; ModuleID = 'diskperf_simpl1_true.cil.o3.bc'
target datalayout = "e-p:32:32:32-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:32:64-f32:32:32-f64:32:64-v64:64:64-v128:128:128-a0:0:64-f80:32:32"
target triple = "i386-unknown-linux-gnu"

declare i32 @__VERIFIER_nondet_int()

define i32 @main() nounwind {
entry:
  %0 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %1 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %2 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %3 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %4 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %5 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %6 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %7 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %8 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %9 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %10 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %11 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %12 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %13 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %14 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %15 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %16 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %17 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %18 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %19 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %20 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %21 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %22 = tail call i32 @ufo.nondet.2() nounwind
  %23 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %24 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %25 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %26 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %27 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %28 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %29 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %30 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %31 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %32 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %33 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %34 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %35 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %36 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %37 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %38 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %39 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %40 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %41 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %42 = tail call i32 @ufo.nondet.2() nounwind
  %43 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %44 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %45 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %46 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %47 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %48 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %49 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %50 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %51 = tail call i1 bitcast (i32 ()* @ufo.nondet.1 to i1 ()*)() nounwind
  %52 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %53 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %54 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %55 = icmp slt i32 %52, 0
  br i1 %55, label %_L___1, label %bb3

bb3:                                              ; preds = %entry
  %56 = icmp eq i32 %54, 0
  %storemerge = select i1 %56, i32 -1073741637, i32 0
  %57 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %58 = icmp eq i32 %57, 0
  br i1 %58, label %_L___1, label %bb4

bb4:                                              ; preds = %bb3
  %59 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %60 = icmp eq i32 %59, 2
  %61 = tail call i32 @__VERIFIER_nondet_int() nounwind
  br i1 %60, label %switch_2_2, label %bb5

bb5:                                              ; preds = %bb4
  %62 = icmp eq i32 %61, 3
  %63 = tail call i32 @__VERIFIER_nondet_int() nounwind
  br i1 %62, label %NodeBlock, label %bb6

bb6:                                              ; preds = %bb5
  %64 = icmp eq i32 %63, 4
  %65 = tail call i32 @__VERIFIER_nondet_int() nounwind
  br i1 %64, label %bb6.i.i19, label %bb7

bb7:                                              ; preds = %bb6
  %66 = icmp eq i32 %65, 12
  br i1 %66, label %bb5.i.i, label %__UFO__1

switch_2_2:                                       ; preds = %bb4
  %67 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %68 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %69 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %70 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %71 = icmp eq i32 %61, 458784
  br i1 %71, label %bb.i32, label %bb5.i.i47

bb.i32:                                           ; preds = %switch_2_2
  %72 = icmp slt i32 %67, %68
  br i1 %72, label %_L___1, label %bb2.i

bb2.i:                                            ; preds = %bb.i32
  %73 = icmp eq i32 %69, 0
  br i1 %73, label %_L___1, label %bb5.i.preheader

bb5.i.preheader:                                  ; preds = %bb2.i
  br label %_L___1

bb5.i.i47:                                        ; preds = %switch_2_2
  %74 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %75 = icmp eq i32 %74, 0
  br i1 %75, label %_L___1, label %bb6.i.i48

bb6.i.i48:                                        ; preds = %bb5.i.i47
  %76 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %77 = icmp eq i32 %76, 1
  br i1 %77, label %_L___1, label %switch_4_default.i.i49

switch_4_default.i.i49:                           ; preds = %bb6.i.i48
  br label %_L___1

NodeBlock:                                        ; preds = %bb5
  %Pivot = icmp slt i32 %63, 2
  br i1 %Pivot, label %LeafBlock, label %LeafBlock48

LeafBlock48:                                      ; preds = %NodeBlock
  %SwitchLeaf49 = icmp eq i32 %63, 2
  br i1 %SwitchLeaf49, label %bb5.i.i.i34.i, label %bb5.i.i9.i

LeafBlock:                                        ; preds = %NodeBlock
  %SwitchLeaf = icmp eq i32 %63, 0
  br i1 %SwitchLeaf, label %bb5.i.i.i.i, label %bb5.i.i9.i

bb5.i.i.i.i:                                      ; preds = %LeafBlock
  %78 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %79 = icmp eq i32 %78, 0
  br i1 %79, label %bb10.i.i.i.i, label %bb6.i.i.i.i

bb6.i.i.i.i:                                      ; preds = %bb5.i.i.i.i
  %80 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %81 = icmp eq i32 %80, 1
  br i1 %81, label %bb10.i.i.i.i, label %bb5.i.i.i

bb10.i.i.i.i:                                     ; preds = %bb6.i.i.i.i, %bb5.i.i.i.i
  %returnVal2.0.i.i.i.i = phi i32 [ 0, %bb5.i.i.i.i ], [ -1073741823, %bb6.i.i.i.i ]
  %82 = icmp eq i32 %returnVal2.0.i.i.i.i, 259
  %storemerge.i.i.i.i = select i1 %82, i32 6, i32 1
  br i1 %82, label %bb5.i.i.i, label %DiskPerfForwardIrpSynchronous.exit.i.i

bb5.i.i.i:                                        ; preds = %bb10.i.i.i.i, %bb6.i.i.i.i
  %returnVal2.0.i.i.i.i.reg2mem.0 = phi i32 [ 259, %bb6.i.i.i.i ], [ %returnVal2.0.i.i.i.i, %bb10.i.i.i.i ]
  %storemerge.i.i.i.i.reg2mem.0 = phi i32 [ 6, %bb6.i.i.i.i ], [ %storemerge.i.i.i.i, %bb10.i.i.i.i ]
  %storemerge.i.i.i.i.reload5 = phi i32 [ 6, %bb6.i.i.i.i ], [ %storemerge.i.i.i.i, %bb10.i.i.i.i ]
  %83 = icmp eq i32 %storemerge.i.i.i.i.reload5, 6
  br i1 %83, label %DiskPerfForwardIrpSynchronous.exit.i.i, label %bb3.i.i.i.i

bb3.i.i.i.i:                                      ; preds = %bb5.i.i.i
  br label %DiskPerfForwardIrpSynchronous.exit.i.i

DiskPerfForwardIrpSynchronous.exit.i.i:           ; preds = %bb3.i.i.i.i, %bb5.i.i.i, %bb10.i.i.i.i
  %returnVal2.0.i.i.i.i.reg2mem.1 = phi i32 [ %returnVal2.0.i.i.i.i.reg2mem.0, %bb3.i.i.i.i ], [ %returnVal2.0.i.i.i.i, %bb10.i.i.i.i ], [ %returnVal2.0.i.i.i.i.reg2mem.0, %bb5.i.i.i ]
  %s.9 = phi i32 [ %storemerge.i.i.i.i.reg2mem.0, %bb3.i.i.i.i ], [ %storemerge.i.i.i.i, %bb10.i.i.i.i ], [ 1, %bb5.i.i.i ]
  %84 = phi i32 [ %storemerge, %bb3.i.i.i.i ], [ %returnVal2.0.i.i.i.i, %bb10.i.i.i.i ], [ %storemerge, %bb5.i.i.i ]
  %85 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %86 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %87 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %88 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %89 = icmp eq i32 %87, 0
  %not.15 = icmp ne i32 %88, 0
  %90 = or i1 %not.15, %89
  br i1 %90, label %DiskPerfRegisterDevice.exit.i.i, label %bb4.i104.i.i.i

bb4.i104.i.i.i:                                   ; preds = %DiskPerfForwardIrpSynchronous.exit.i.i
  %91 = icmp eq i32 %s.9, 1
  br i1 %91, label %bb5.i107.i.i.i, label %UnifiedReturnBlock

bb5.i107.i.i.i:                                   ; preds = %bb4.i104.i.i.i
  %92 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %93 = icmp eq i32 %92, 0
  br i1 %93, label %bb10.i116.i.i.i, label %bb6.i108.i.i.i

bb6.i108.i.i.i:                                   ; preds = %bb5.i107.i.i.i
  %94 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %95 = icmp eq i32 %94, 1
  br i1 %95, label %bb10.i116.i.i.i, label %switch_4_default.i109.i.i.i

switch_4_default.i109.i.i.i:                      ; preds = %bb6.i108.i.i.i
  br label %bb10.i116.i.i.i

bb10.i116.i.i.i:                                  ; preds = %switch_4_default.i109.i.i.i, %bb6.i108.i.i.i, %bb5.i107.i.i.i
  %returnVal2.0.i110.i.i.i = phi i32 [ 259, %switch_4_default.i109.i.i.i ], [ 0, %bb5.i107.i.i.i ], [ -1073741823, %bb6.i108.i.i.i ]
  %96 = icmp eq i32 %returnVal2.0.i110.i.i.i, 259
  %storemerge.i115.i.i.i = select i1 %96, i32 6, i32 1
  %s.15 = select i1 %96, i32 1, i32 %storemerge.i115.i.i.i
  %status.0.i.i.i = select i1 %96, i32 %85, i32 %returnVal2.0.i110.i.i.i
  %.not = icmp sgt i32 %status.0.i.i.i, -1
  %97 = icmp eq i32 %86, 0
  %or.cond24 = or i1 %.not, %97
  br i1 %or.cond24, label %DiskPerfRegisterDevice.exit.i.i, label %bb6.i.i.i

bb6.i.i.i:                                        ; preds = %bb10.i116.i.i.i
  %98 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %99 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %100 = icmp eq i32 %98, 0
  %not.14 = icmp ne i32 %99, 0
  %101 = or i1 %not.14, %100
  br i1 %101, label %DiskPerfRegisterDevice.exit.i.i, label %bb4.i66.i.i.i

bb4.i66.i.i.i:                                    ; preds = %bb6.i.i.i
  %102 = icmp eq i32 %s.15, 1
  br i1 %102, label %bb5.i69.i.i.i, label %UnifiedReturnBlock

bb5.i69.i.i.i:                                    ; preds = %bb4.i66.i.i.i
  %103 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %104 = icmp eq i32 %103, 0
  br i1 %104, label %bb10.i78.i.i.i, label %bb6.i70.i.i.i

bb6.i70.i.i.i:                                    ; preds = %bb5.i69.i.i.i
  %105 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %106 = icmp eq i32 %105, 1
  br i1 %106, label %bb10.i78.i.i.i, label %switch_4_default.i71.i.i.i

switch_4_default.i71.i.i.i:                       ; preds = %bb6.i70.i.i.i
  br label %bb10.i78.i.i.i

bb10.i78.i.i.i:                                   ; preds = %switch_4_default.i71.i.i.i, %bb6.i70.i.i.i, %bb5.i69.i.i.i
  %returnVal2.0.i72.i.i.i = phi i32 [ 259, %switch_4_default.i71.i.i.i ], [ 0, %bb5.i69.i.i.i ], [ -1073741823, %bb6.i70.i.i.i ]
  %107 = icmp eq i32 %returnVal2.0.i72.i.i.i, 259
  %storemerge.i77.i.i.i = select i1 %107, i32 6, i32 1
  %s.19 = select i1 %107, i32 1, i32 %storemerge.i77.i.i.i
  %status.2.i.i.i = select i1 %107, i32 %85, i32 %returnVal2.0.i72.i.i.i
  %108 = icmp eq i32 %status.2.i.i.i, -2147483643
  br i1 %108, label %bb11.i.i.i, label %bb17.i.i.i

bb11.i.i.i:                                       ; preds = %bb10.i78.i.i.i
  br i1 %97, label %DiskPerfRegisterDevice.exit.i.i, label %bb13.i.i.i

bb13.i.i.i:                                       ; preds = %bb11.i.i.i
  %109 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %110 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %111 = icmp eq i32 %109, 0
  %not. = icmp ne i32 %110, 0
  %112 = or i1 %not., %111
  br i1 %112, label %DiskPerfRegisterDevice.exit.i.i, label %bb4.i28.i.i.i

bb4.i28.i.i.i:                                    ; preds = %bb13.i.i.i
  %113 = icmp eq i32 %s.19, 1
  br i1 %113, label %bb5.i31.i.i.i, label %UnifiedReturnBlock

bb5.i31.i.i.i:                                    ; preds = %bb4.i28.i.i.i
  %114 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %115 = icmp eq i32 %114, 0
  br i1 %115, label %bb17.i.i.i, label %bb6.i32.i.i.i

bb6.i32.i.i.i:                                    ; preds = %bb5.i31.i.i.i
  %116 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %117 = icmp eq i32 %116, 1
  br i1 %117, label %bb17.i.i.i, label %bb16.i.i.i

bb16.i.i.i:                                       ; preds = %bb6.i32.i.i.i
  br label %bb17.i.i.i

bb17.i.i.i:                                       ; preds = %bb16.i.i.i, %bb6.i32.i.i.i, %bb5.i31.i.i.i, %bb10.i78.i.i.i
  %s.21 = phi i32 [ 1, %bb16.i.i.i ], [ %s.19, %bb10.i78.i.i.i ], [ 1, %bb5.i31.i.i.i ], [ 1, %bb6.i32.i.i.i ]
  %lowerDriverReturn.11 = phi i32 [ 259, %bb16.i.i.i ], [ %returnVal2.0.i72.i.i.i, %bb10.i78.i.i.i ], [ 0, %bb5.i31.i.i.i ], [ -1073741823, %bb6.i32.i.i.i ]
  %status.3.i.i.i = phi i32 [ %85, %bb16.i.i.i ], [ %status.2.i.i.i, %bb10.i78.i.i.i ], [ 0, %bb5.i31.i.i.i ], [ -1073741823, %bb6.i32.i.i.i ]
  %118 = icmp slt i32 %status.3.i.i.i, 0
  br i1 %118, label %DiskPerfRegisterDevice.exit.i.i, label %bb19.i.i.i

bb19.i.i.i:                                       ; preds = %bb17.i.i.i
  %119 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %120 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %121 = icmp eq i32 %119, 0
  %not.13 = icmp ne i32 %120, 0
  %122 = or i1 %not.13, %121
  br i1 %122, label %DiskPerfRegisterDevice.exit.i.i, label %bb4.i6.i.i.i

bb4.i6.i.i.i:                                     ; preds = %bb19.i.i.i
  %123 = icmp eq i32 %s.21, 1
  br i1 %123, label %bb5.i.i16.i.i, label %UnifiedReturnBlock

bb5.i.i16.i.i:                                    ; preds = %bb4.i6.i.i.i
  %124 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %125 = icmp eq i32 %124, 0
  br i1 %125, label %_L___1, label %bb6.i.i17.i.i

bb6.i.i17.i.i:                                    ; preds = %bb5.i.i16.i.i
  %126 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %127 = icmp eq i32 %126, 1
  br i1 %127, label %DiskPerfRegisterDevice.exit.i.i, label %_L___1

DiskPerfRegisterDevice.exit.i.i:                  ; preds = %bb6.i.i17.i.i, %bb19.i.i.i, %bb17.i.i.i, %bb13.i.i.i, %bb11.i.i.i, %bb6.i.i.i, %bb10.i116.i.i.i, %DiskPerfForwardIrpSynchronous.exit.i.i
  %s.12 = phi i32 [ %s.9, %DiskPerfForwardIrpSynchronous.exit.i.i ], [ %s.15, %bb10.i116.i.i.i ], [ %s.15, %bb6.i.i.i ], [ %s.19, %bb11.i.i.i ], [ %s.19, %bb13.i.i.i ], [ %s.21, %bb17.i.i.i ], [ %s.21, %bb19.i.i.i ], [ 1, %bb6.i.i17.i.i ]
  %lowerDriverReturn.8 = phi i32 [ %returnVal2.0.i.i.i.i.reg2mem.1, %DiskPerfForwardIrpSynchronous.exit.i.i ], [ %returnVal2.0.i110.i.i.i, %bb10.i116.i.i.i ], [ %returnVal2.0.i110.i.i.i, %bb6.i.i.i ], [ %returnVal2.0.i72.i.i.i, %bb11.i.i.i ], [ %returnVal2.0.i72.i.i.i, %bb13.i.i.i ], [ %lowerDriverReturn.11, %bb17.i.i.i ], [ %lowerDriverReturn.11, %bb19.i.i.i ], [ -1073741823, %bb6.i.i17.i.i ]
  %128 = icmp eq i32 %s.12, 1
  br i1 %128, label %_L___1, label %UnifiedReturnBlock

bb5.i.i.i34.i:                                    ; preds = %LeafBlock48
  %129 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %130 = icmp eq i32 %129, 0
  br i1 %130, label %bb10.i.i.i43.i, label %bb6.i.i.i35.i

bb6.i.i.i35.i:                                    ; preds = %bb5.i.i.i34.i
  %131 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %132 = icmp eq i32 %131, 1
  br i1 %132, label %bb10.i.i.i43.i, label %bb5.i.i48.i

bb10.i.i.i43.i:                                   ; preds = %bb6.i.i.i35.i, %bb5.i.i.i34.i
  %returnVal2.0.i.i.i37.i = phi i32 [ 0, %bb5.i.i.i34.i ], [ -1073741823, %bb6.i.i.i35.i ]
  %133 = icmp eq i32 %returnVal2.0.i.i.i37.i, 259
  %storemerge.i.i.i42.i = select i1 %133, i32 6, i32 1
  br i1 %133, label %bb5.i.i48.i, label %DiskPerfForwardIrpSynchronous.exit.i58.i

bb5.i.i48.i:                                      ; preds = %bb10.i.i.i43.i, %bb6.i.i.i35.i
  %returnVal2.0.i.i.i37.i.reg2mem.0 = phi i32 [ 259, %bb6.i.i.i35.i ], [ %returnVal2.0.i.i.i37.i, %bb10.i.i.i43.i ]
  %storemerge.i.i.i42.i.reg2mem.0 = phi i32 [ 6, %bb6.i.i.i35.i ], [ %storemerge.i.i.i42.i, %bb10.i.i.i43.i ]
  %storemerge.i.i.i42.i.reload38 = phi i32 [ 6, %bb6.i.i.i35.i ], [ %storemerge.i.i.i42.i, %bb10.i.i.i43.i ]
  %134 = icmp eq i32 %storemerge.i.i.i42.i.reload38, 6
  br i1 %134, label %_L___1, label %DiskPerfForwardIrpSynchronous.exit.i58.i

DiskPerfForwardIrpSynchronous.exit.i58.i:         ; preds = %bb5.i.i48.i, %bb10.i.i.i43.i
  %returnVal2.0.i.i.i37.i.reg2mem.1 = phi i32 [ %returnVal2.0.i.i.i37.i, %bb10.i.i.i43.i ], [ %returnVal2.0.i.i.i37.i.reg2mem.0, %bb5.i.i48.i ]
  %s.30 = phi i32 [ %storemerge.i.i.i42.i, %bb10.i.i.i43.i ], [ %storemerge.i.i.i42.i.reg2mem.0, %bb5.i.i48.i ]
  %135 = phi i32 [ %returnVal2.0.i.i.i37.i, %bb10.i.i.i43.i ], [ %storemerge, %bb5.i.i48.i ]
  %136 = icmp eq i32 %s.30, 1
  br i1 %136, label %_L___1, label %UnifiedReturnBlock

bb5.i.i9.i:                                       ; preds = %LeafBlock, %LeafBlock48
  %137 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %138 = icmp eq i32 %137, 0
  br i1 %138, label %_L___1, label %bb6.i.i10.i

bb6.i.i10.i:                                      ; preds = %bb5.i.i9.i
  %139 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %140 = icmp eq i32 %139, 1
  br i1 %140, label %_L___1, label %switch_4_default.i.i.i

switch_4_default.i.i.i:                           ; preds = %bb6.i.i10.i
  br label %_L___1

bb6.i.i19:                                        ; preds = %bb6
  %141 = icmp eq i32 %65, 0
  br i1 %141, label %_L___1, label %bb7.i.i

bb7.i.i:                                          ; preds = %bb6.i.i19
  %142 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %143 = icmp eq i32 %142, 1
  br i1 %143, label %_L___1, label %switch_6_default.i.i

switch_6_default.i.i:                             ; preds = %bb7.i.i
  br label %_L___1

bb5.i.i:                                          ; preds = %bb7
  %144 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %145 = icmp eq i32 %144, 0
  br i1 %145, label %_L___1, label %bb6.i.i

bb6.i.i:                                          ; preds = %bb5.i.i
  %146 = tail call i32 @__VERIFIER_nondet_int() nounwind
  %147 = icmp eq i32 %146, 1
  br i1 %147, label %_L___1, label %switch_4_default.i.i

switch_4_default.i.i:                             ; preds = %bb6.i.i
  br label %_L___1

__UFO__1:                                         ; preds = %__UFO__1, %bb7
  br label %__UFO__1

_L___1:                                           ; preds = %switch_4_default.i.i, %bb6.i.i, %bb5.i.i, %switch_6_default.i.i, %bb7.i.i, %bb6.i.i19, %switch_4_default.i.i.i, %bb6.i.i10.i, %bb5.i.i9.i, %DiskPerfForwardIrpSynchronous.exit.i58.i, %bb5.i.i48.i, %DiskPerfRegisterDevice.exit.i.i, %bb6.i.i17.i.i, %bb5.i.i16.i.i, %switch_4_default.i.i49, %bb6.i.i48, %bb5.i.i47, %bb5.i.preheader, %bb2.i, %bb.i32, %bb3, %entry
  %s.0 = phi i32 [ 4, %switch_4_default.i.i.i ], [ 4, %switch_6_default.i.i ], [ 7, %switch_4_default.i.i49 ], [ 7, %switch_4_default.i.i ], [ 0, %entry ], [ 2, %bb3 ], [ 2, %bb.i32 ], [ 2, %bb2.i ], [ 7, %bb5.i.i47 ], [ 7, %bb6.i.i48 ], [ 2, %bb5.i.i16.i.i ], [ 2, %bb6.i.i17.i.i ], [ 2, %DiskPerfRegisterDevice.exit.i.i ], [ 2, %bb5.i.i48.i ], [ 2, %DiskPerfForwardIrpSynchronous.exit.i58.i ], [ 4, %bb5.i.i9.i ], [ 4, %bb6.i.i10.i ], [ 4, %bb6.i.i19 ], [ 4, %bb7.i.i ], [ 7, %bb5.i.i ], [ 7, %bb6.i.i ], [ 2, %bb5.i.preheader ]
  %lowerDriverReturn.0 = phi i32 [ 259, %switch_4_default.i.i.i ], [ 259, %switch_6_default.i.i ], [ 259, %switch_4_default.i.i49 ], [ 259, %switch_4_default.i.i ], [ 0, %entry ], [ 0, %bb3 ], [ 0, %bb.i32 ], [ 0, %bb2.i ], [ 0, %bb5.i.i47 ], [ -1073741823, %bb6.i.i48 ], [ 0, %bb5.i.i16.i.i ], [ 259, %bb6.i.i17.i.i ], [ %lowerDriverReturn.8, %DiskPerfRegisterDevice.exit.i.i ], [ %returnVal2.0.i.i.i37.i.reg2mem.0, %bb5.i.i48.i ], [ %returnVal2.0.i.i.i37.i.reg2mem.1, %DiskPerfForwardIrpSynchronous.exit.i58.i ], [ 0, %bb5.i.i9.i ], [ -1073741823, %bb6.i.i10.i ], [ 0, %bb6.i.i19 ], [ -1073741823, %bb7.i.i ], [ 0, %bb5.i.i ], [ -1073741823, %bb6.i.i ], [ 0, %bb5.i.preheader ]
  %status.1 = phi i32 [ 259, %switch_4_default.i.i.i ], [ 259, %switch_6_default.i.i ], [ 259, %switch_4_default.i.i49 ], [ 259, %switch_4_default.i.i ], [ %52, %entry ], [ 0, %bb3 ], [ -1073741789, %bb.i32 ], [ -1073741823, %bb2.i ], [ 0, %bb5.i.i47 ], [ -1073741823, %bb6.i.i48 ], [ %84, %bb5.i.i16.i.i ], [ %84, %bb6.i.i17.i.i ], [ %84, %DiskPerfRegisterDevice.exit.i.i ], [ %storemerge, %bb5.i.i48.i ], [ %135, %DiskPerfForwardIrpSynchronous.exit.i58.i ], [ 0, %bb5.i.i9.i ], [ -1073741823, %bb6.i.i10.i ], [ 0, %bb6.i.i19 ], [ -1073741823, %bb7.i.i ], [ 0, %bb5.i.i ], [ -1073741823, %bb6.i.i ], [ 0, %bb5.i.preheader ]
  %148 = icmp eq i32 %s.0, 0
  %149 = icmp eq i32 %status.1, -1
  %or.cond = or i1 %149, %148
  br i1 %or.cond, label %__UFO__2, label %NodeBlock59

NodeBlock59:                                      ; preds = %_L___1
  %Pivot60 = icmp ult i32 %s.0, 4
  br i1 %Pivot60, label %LeafBlock51, label %NodeBlock66

NodeBlock66:                                      ; preds = %NodeBlock59
  switch i32 %s.0, label %UnifiedReturnBlock [
    i32 7, label %bb27
    i32 4, label %bb27
  ]

LeafBlock51:                                      ; preds = %NodeBlock59
  %SwitchLeaf52.not = icmp ne i32 %s.0, 2
  %150 = icmp eq i32 %status.1, 259
  %or.cond61 = or i1 %150, %SwitchLeaf52.not
  br i1 %or.cond61, label %UnifiedReturnBlock, label %__UFO__2

bb27:                                             ; preds = %NodeBlock66, %NodeBlock66
  %151 = icmp eq i32 %status.1, %lowerDriverReturn.0
  br i1 %151, label %__UFO__2, label %UnifiedReturnBlock

__UFO__2:                                         ; preds = %__UFO__2, %bb27, %LeafBlock51, %_L___1
  br label %__UFO__2

UnifiedReturnBlock:                               ; preds = %bb27, %LeafBlock51, %NodeBlock66, %DiskPerfForwardIrpSynchronous.exit.i58.i, %DiskPerfRegisterDevice.exit.i.i, %bb4.i6.i.i.i, %bb4.i28.i.i.i, %bb4.i66.i.i.i, %bb4.i104.i.i.i
  ret i32 42
}

declare i32 @ufo.nondet.1()

declare i32 @ufo.nondet.2()
