procedure {:kernel} lbm(_param_dirX: double_8, _param_dirY: double_8, _param_omega: double);
  requires !_READ_HAS_OCCURRED__ARRAY_if0$1 && !_WRITE_HAS_OCCURRED__ARRAY_if0$1 && !_WRITE_HAS_OCCURRED__ARRAY_if0$2;
  requires !_READ_HAS_OCCURRED__ARRAY_of0$1 && !_WRITE_HAS_OCCURRED__ARRAY_of0$1 && !_WRITE_HAS_OCCURRED__ARRAY_of0$2;
  requires !_READ_HAS_OCCURRED__ARRAY_if1234$1 && !_WRITE_HAS_OCCURRED__ARRAY_if1234$1 && !_WRITE_HAS_OCCURRED__ARRAY_if1234$2;
  requires !_READ_HAS_OCCURRED__ARRAY_of1234$1 && !_WRITE_HAS_OCCURRED__ARRAY_of1234$1 && !_WRITE_HAS_OCCURRED__ARRAY_of1234$2;
  requires !_READ_HAS_OCCURRED__ARRAY_if5678$1 && !_WRITE_HAS_OCCURRED__ARRAY_if5678$1 && !_WRITE_HAS_OCCURRED__ARRAY_if5678$2;
  requires !_READ_HAS_OCCURRED__ARRAY_of5678$1 && !_WRITE_HAS_OCCURRED__ARRAY_of5678$1 && !_WRITE_HAS_OCCURRED__ARRAY_of5678$2;
  requires !_READ_HAS_OCCURRED__ARRAY_typeVar$1 && !_WRITE_HAS_OCCURRED__ARRAY_typeVar$1 && !_WRITE_HAS_OCCURRED__ARRAY_typeVar$2;
  requires !_READ_HAS_OCCURRED__ARRAY_velocityBuffer$1 && !_WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$1 && !_WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$2;
  requires BV32_GT(get_local_size.0, 0bv32);
  requires BV32_GT(get_num_groups.0, 0bv32);
  requires BV32_GEQ(get_group_id.0, 0bv32);
  requires BV32_LT(get_group_id.0, get_num_groups.0);
  requires BV32_GT(get_local_size.1, 0bv32);
  requires BV32_GT(get_num_groups.1, 0bv32);
  requires BV32_GEQ(get_group_id.1, 0bv32);
  requires BV32_LT(get_group_id.1, get_num_groups.1);
  requires BV32_GT(get_local_size.2, 0bv32);
  requires BV32_GT(get_num_groups.2, 0bv32);
  requires BV32_GEQ(get_group_id.2, 0bv32);
  requires BV32_LT(get_group_id.2, get_num_groups.2);
  requires get_local_id.0$1 != get_local_id.0$2 || get_local_id.1$1 != get_local_id.1$2 || get_local_id.2$1 != get_local_id.2$2;
  requires BV32_GEQ(get_local_id.0$1, 0bv32) && BV32_GEQ(get_local_id.0$2, 0bv32) && BV32_LT(get_local_id.0$1, get_local_size.0) && BV32_LT(get_local_id.0$2, get_local_size.0) && BV32_GEQ(get_local_id.1$1, 0bv32) && BV32_GEQ(get_local_id.1$2, 0bv32) && BV32_LT(get_local_id.1$1, get_local_size.1) && BV32_LT(get_local_id.1$2, get_local_size.1) && BV32_GEQ(get_local_id.2$1, 0bv32) && BV32_GEQ(get_local_id.2$2, 0bv32) && BV32_LT(get_local_id.2$1, get_local_size.2) && BV32_LT(get_local_id.2$2, get_local_size.2);



implementation {:kernel} lbm(_param_dirX: double_8, _param_dirY: double_8, _param_omega: double)
{
  var dirX: double_8;
  var dirY: double_8;
  var omega: double;
  var _call_temp1$1: double;
  var _call_temp1$2: double;
  var _call_temp2$1: double;
  var _call_temp2$2: double;
  var _call_temp3$1: double;
  var _call_temp3$2: double;
  var _call_temp4$1: double;
  var _call_temp4$2: double;
  var _call_temp5$1: double;
  var _call_temp5$2: double;
  var _call_temp6$1: double;
  var _call_temp6$2: double;
  var _call_temp7$1: double;
  var _call_temp7$2: double;
  var _call_temp8$1: double;
  var _call_temp8$2: double;
  var _call_temp9$1: double;
  var _call_temp9$2: double;
  var _read_temp1$1: double;
  var _read_temp1$2: double;
  var _read_temp10$1: double_4;
  var _read_temp10$2: double_4;
  var _read_temp11$1: double_4;
  var _read_temp11$2: double_4;
  var _read_temp12$1: double_4;
  var _read_temp12$2: double_4;
  var _read_temp13$1: double_4;
  var _read_temp13$2: double_4;
  var _read_temp14$1: double_2;
  var _read_temp14$2: double_2;
  var _read_temp15$1: double_2;
  var _read_temp15$2: double_2;
  var _read_temp16$1: double_2;
  var _read_temp16$2: double_2;
  var _read_temp17$1: double;
  var _read_temp17$2: double;
  var _read_temp18$1: double;
  var _read_temp18$2: double;
  var _read_temp19$1: double;
  var _read_temp19$2: double;
  var _read_temp2$1: double;
  var _read_temp2$2: double;
  var _read_temp20$1: double;
  var _read_temp20$2: double;
  var _read_temp21$1: double;
  var _read_temp21$2: double;
  var _read_temp22$1: double;
  var _read_temp22$2: double;
  var _read_temp23$1: double;
  var _read_temp23$2: double;
  var _read_temp24$1: double;
  var _read_temp24$2: double;
  var _read_temp25$1: double;
  var _read_temp25$2: double;
  var _read_temp26$1: double;
  var _read_temp26$2: double;
  var _read_temp27$1: double;
  var _read_temp27$2: double;
  var _read_temp28$1: double;
  var _read_temp28$2: double;
  var _read_temp29$1: double;
  var _read_temp29$2: double;
  var _read_temp3$1: double_4;
  var _read_temp3$2: double_4;
  var _read_temp30$1: double;
  var _read_temp30$2: double;
  var _read_temp31$1: double;
  var _read_temp31$2: double;
  var _read_temp32$1: double;
  var _read_temp32$2: double;
  var _read_temp33$1: double;
  var _read_temp33$2: double;
  var _read_temp34$1: double;
  var _read_temp34$2: double;
  var _read_temp35$1: double;
  var _read_temp35$2: double;
  var _read_temp36$1: double_4;
  var _read_temp36$2: double_4;
  var _read_temp37$1: double_4;
  var _read_temp37$2: double_4;
  var _read_temp38$1: double_4;
  var _read_temp38$2: double_4;
  var _read_temp39$1: double_4;
  var _read_temp39$2: double_4;
  var _read_temp4$1: double_4;
  var _read_temp4$2: double_4;
  var _read_temp40$1: double_4;
  var _read_temp40$2: double_4;
  var _read_temp41$1: double_4;
  var _read_temp41$2: double_4;
  var _read_temp42$1: double_4;
  var _read_temp42$2: double_4;
  var _read_temp43$1: double_4;
  var _read_temp43$2: double_4;
  var _read_temp44$1: double_4;
  var _read_temp44$2: double_4;
  var _read_temp45$1: double_4;
  var _read_temp45$2: double_4;
  var _read_temp46$1: double_4;
  var _read_temp46$2: double_4;
  var _read_temp47$1: double_4;
  var _read_temp47$2: double_4;
  var _read_temp48$1: bv32_8;
  var _read_temp48$2: bv32_8;
  var _read_temp49: bv32_8;
  var _read_temp5$1: double_4;
  var _read_temp5$2: double_4;
  var _read_temp50$1: bv32_8;
  var _read_temp50$2: bv32_8;
  var _read_temp51: bv32_8;
  var _read_temp52$1: bv32_8;
  var _read_temp52$2: bv32_8;
  var _read_temp53: bv32_8;
  var _read_temp54$1: bv32_8;
  var _read_temp54$2: bv32_8;
  var _read_temp55: bv32_8;
  var _read_temp56: bv32_8;
  var _read_temp57$1: bv32_8;
  var _read_temp57$2: bv32_8;
  var _read_temp58$1: bv32_8;
  var _read_temp58$2: bv32_8;
  var _read_temp59$1: bv32_8;
  var _read_temp59$2: bv32_8;
  var _read_temp6$1: double_4;
  var _read_temp6$2: double_4;
  var _read_temp60: bv32_8;
  var _read_temp61$1: bv32_8;
  var _read_temp61$2: bv32_8;
  var _read_temp62$1: bv32_8;
  var _read_temp62$2: bv32_8;
  var _read_temp63$1: bv32_8;
  var _read_temp63$2: bv32_8;
  var _read_temp64$1: double_4;
  var _read_temp64$2: double_4;
  var _read_temp65$1: double;
  var _read_temp65$2: double;
  var _read_temp66$1: double_4;
  var _read_temp66$2: double_4;
  var _read_temp67$1: double;
  var _read_temp67$2: double;
  var _read_temp68$1: double_4;
  var _read_temp68$2: double_4;
  var _read_temp69$1: double;
  var _read_temp69$2: double;
  var _read_temp7$1: bool;
  var _read_temp7$2: bool;
  var _read_temp70$1: double_4;
  var _read_temp70$2: double_4;
  var _read_temp71$1: double;
  var _read_temp71$2: double;
  var _read_temp72$1: double_4;
  var _read_temp72$2: double_4;
  var _read_temp73$1: double;
  var _read_temp73$2: double;
  var _read_temp74$1: double_4;
  var _read_temp74$2: double_4;
  var _read_temp75$1: double;
  var _read_temp75$2: double;
  var _read_temp76$1: double_4;
  var _read_temp76$2: double_4;
  var _read_temp77$1: double;
  var _read_temp77$2: double;
  var _read_temp78$1: double_4;
  var _read_temp78$2: double_4;
  var _read_temp79$1: double;
  var _read_temp79$2: double;
  var _read_temp8$1: double_4;
  var _read_temp8$2: double_4;
  var _read_temp9$1: double_4;
  var _read_temp9$2: double_4;
  var f0$1: double;
  var f0$2: double;
  var f1234$1: double_4;
  var f1234$2: double_4;
  var f5678$1: double_4;
  var f5678$2: double_4;
  var fEq0$1: double;
  var fEq0$2: double;
  var fEq1234$1: double_4;
  var fEq1234$2: double_4;
  var fEq5678$1: double_4;
  var fEq5678$2: double_4;
  var id$1: bv32_2;
  var id$2: bv32_2;
  var if0: _POINTER_TO_global_double;
  var if1234: _POINTER_TO_global_double_4;
  var if5678: _POINTER_TO_global_double_4;
  var nPos$1: bv32_8;
  var nPos$2: bv32_8;
  var nX$1: bv32_8;
  var nX$2: bv32_8;
  var nY$1: bv32_8;
  var nY$2: bv32_8;
  var of0: _POINTER_TO_global_double;
  var of1234: _POINTER_TO_global_double_4;
  var of5678: _POINTER_TO_global_double_4;
  var pos$1: bv32;
  var pos$2: bv32;
  var rho$1: double;
  var rho$2: double;
  var t1$1: bv32;
  var t1$2: bv32;
  var t2$1: bv32;
  var t2$2: bv32;
  var t3$1: bv32;
  var t3$2: bv32;
  var t4$1: bv32;
  var t4$2: bv32;
  var temp$1: double_4;
  var temp$2: double_4;
  var typeVar: _POINTER_TO_global_bool;
  var u$1: double_2;
  var u$2: double_2;
  var velocityBuffer: _POINTER_TO_global_double_2;
  var weight: _POINTER_TO_constant_double;
  var width: bv32;
  var _P0$1: bool;
  var _P0$2: bool;
  var _P1$1: bool;
  var _P1$2: bool;
  var _P2$1: bool;
  var _P2$2: bool;
  var _P3$1: bool;
  var _P3$2: bool;
  var _P4$1: bool;
  var _P4$2: bool;
  var _P5$1: bool;
  var _P5$2: bool;
  var _P6$1: bool;
  var _P6$2: bool;
  var _P7$1: bool;
  var _P7$2: bool;
  var _P8$1: bool;
  var _P8$2: bool;
  var _P9$1: bool;
  var _P9$2: bool;
  var _P10$1: bool;
  var _P10$2: bool;
  var _P11$1: bool;
  var _P11$2: bool;
  var _P12$1: bool;
  var _P12$2: bool;
  var _P13$1: bool;
  var _P13$2: bool;
  var _P14$1: bool;
  var _P14$2: bool;
  var _P15$1: bool;
  var _P15$2: bool;
  var _P16$1: bool;
  var _P16$2: bool;
  var _P17$1: bool;
  var _P17$2: bool;
  var _P18$1: bool;
  var _P18$2: bool;
  var _P19$1: bool;
  var _P19$2: bool;
  var _P20$1: bool;
  var _P20$2: bool;
  var _P21$1: bool;
  var _P21$2: bool;
  var _P22$1: bool;
  var _P22$2: bool;
  var _P23$1: bool;
  var _P23$2: bool;
  var _P24$1: bool;
  var _P24$2: bool;
  var _P25$1: bool;
  var _P25$2: bool;
  var _P26$1: bool;
  var _P26$2: bool;
  var _P27$1: bool;
  var _P27$2: bool;
  var _P28$1: bool;
  var _P28$2: bool;
  var _P29$1: bool;
  var _P29$2: bool;
  var _P30$1: bool;
  var _P30$2: bool;
  var _P31$1: bool;
  var _P31$2: bool;
  var _P32$1: bool;
  var _P32$2: bool;
  var _P33$1: bool;
  var _P33$2: bool;
  var _HAVOC_double_4$1: double_4;
  var _HAVOC_double_4$2: double_4;

  anon0:
    call barrier(true, true);
    dirX := _param_dirX;
    dirY := _param_dirY;
    omega := _param_omega;
    if0 := _CONSTRUCT_POINTER_TO_global_double(_ARRAY_if0_BASE, 0bv32);
    if1234 := _CONSTRUCT_POINTER_TO_global_double_4(_ARRAY_if1234_BASE, 0bv32);
    if5678 := _CONSTRUCT_POINTER_TO_global_double_4(_ARRAY_if5678_BASE, 0bv32);
    of0 := _CONSTRUCT_POINTER_TO_global_double(_ARRAY_of0_BASE, 0bv32);
    of1234 := _CONSTRUCT_POINTER_TO_global_double_4(_ARRAY_of1234_BASE, 0bv32);
    of5678 := _CONSTRUCT_POINTER_TO_global_double_4(_ARRAY_of5678_BASE, 0bv32);
    typeVar := _CONSTRUCT_POINTER_TO_global_bool(_ARRAY_typeVar_BASE, 0bv32);
    velocityBuffer := _CONSTRUCT_POINTER_TO_global_double_2(_ARRAY_velocityBuffer_BASE, 0bv32);
    weight := _CONSTRUCT_POINTER_TO_constant_double(_ARRAY_weight_BASE, 0bv32);
    id$1, id$2 := construct_bv32_2.1_1(BV32_ADD(BV32_MUL(get_group_id.0, get_local_size.0), get_local_id.0$1), BV32_ADD(BV32_MUL(get_group_id.1, get_local_size.1), get_local_id.1$1)), construct_bv32_2.1_1(BV32_ADD(BV32_MUL(get_group_id.0, get_local_size.0), get_local_id.0$2), BV32_ADD(BV32_MUL(get_group_id.1, get_local_size.1), get_local_id.1$2));
    width := BV32_MUL(get_local_size.0, get_num_groups.0);
    pos$1, pos$2 := BV32_ADD(bv32_2_extract_0(id$1), BV32_MUL(width, bv32_2_extract_1(id$1))), BV32_ADD(bv32_2_extract_0(id$2), BV32_MUL(width, bv32_2_extract_1(id$2)));
    if (base#_CONSTRUCT_POINTER_TO_global_double(if0) == _ARRAY_if0_BASE)
    {
      anon113_Then:
        havoc _read_temp1$1, _read_temp1$2;
        call _LOG_READ__ARRAY_if0(true, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double(if0), pos$1));
    }
    else
    {
      anon113_Else:
        assert false && false;
    }

  anon3:
    if (base#_CONSTRUCT_POINTER_TO_global_double(if0) == _ARRAY_if0_BASE)
    {
      anon114_Then:
        havoc _read_temp2$1, _read_temp2$2;
        call _LOG_READ__ARRAY_if0(true, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double(if0), pos$1));
    }
    else
    {
      anon114_Else:
        assert false && false;
    }

  anon6:
    f0$1, f0$2 := _read_temp2$1, _read_temp2$2;
    if (base#_CONSTRUCT_POINTER_TO_global_double_4(if1234) == _ARRAY_if1234_BASE)
    {
      anon115_Then:
        havoc _read_temp3$1, _read_temp3$2;
        call _LOG_READ__ARRAY_if1234(true, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(if1234), pos$1));
    }
    else
    {
      anon115_Else:
        assert false && false;
    }

  anon9:
    if (base#_CONSTRUCT_POINTER_TO_global_double_4(if1234) == _ARRAY_if1234_BASE)
    {
      anon116_Then:
        havoc _read_temp4$1, _read_temp4$2;
        call _LOG_READ__ARRAY_if1234(true, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(if1234), pos$1));
    }
    else
    {
      anon116_Else:
        assert false && false;
    }

  anon12:
    f1234$1, f1234$2 := _read_temp4$1, _read_temp4$2;
    if (base#_CONSTRUCT_POINTER_TO_global_double_4(if5678) == _ARRAY_if5678_BASE)
    {
      anon117_Then:
        havoc _read_temp5$1, _read_temp5$2;
        call _LOG_READ__ARRAY_if5678(true, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(if5678), pos$1));
    }
    else
    {
      anon117_Else:
        assert false && false;
    }

  anon15:
    if (base#_CONSTRUCT_POINTER_TO_global_double_4(if5678) == _ARRAY_if5678_BASE)
    {
      anon118_Then:
        havoc _read_temp6$1, _read_temp6$2;
        call _LOG_READ__ARRAY_if5678(true, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(if5678), pos$1));
    }
    else
    {
      anon118_Else:
        assert false && false;
    }

  anon18:
    f5678$1, f5678$2 := _read_temp6$1, _read_temp6$2;
    if (base#_CONSTRUCT_POINTER_TO_global_bool(typeVar) == _ARRAY_typeVar_BASE)
    {
      anon119_Then:
        _read_temp7$1, _read_temp7$2 := _ARRAY_typeVar$1[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_bool(typeVar), pos$1)], _ARRAY_typeVar$2[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_bool(typeVar), pos$2)];
        call _LOG_READ__ARRAY_typeVar(true, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_bool(typeVar), pos$1));
    }
    else
    {
      anon119_Else:
        assert false && false;
    }

  anon21:
    _P0$1, _P0$2 := _read_temp7$1, _read_temp7$2;

  anon120_Then:
    _read_temp8$1, _read_temp8$2 := (if _P0$1 then construct_double_4.1_1_1_1(double_4_extract_2(f1234$1), double_4_extract_3(f1234$1), double_4_extract_0(f1234$1), double_4_extract_1(f1234$1)) else _read_temp8$1), (if _P0$2 then construct_double_4.1_1_1_1(double_4_extract_2(f1234$2), double_4_extract_3(f1234$2), double_4_extract_0(f1234$2), double_4_extract_1(f1234$2)) else _read_temp8$2);
    f1234$1, f1234$2 := (if _P0$1 then construct_double_4.1_1_1_1(double_4_extract_0(_read_temp8$1), double_4_extract_1(_read_temp8$1), double_4_extract_2(_read_temp8$1), double_4_extract_3(_read_temp8$1)) else f1234$1), (if _P0$2 then construct_double_4.1_1_1_1(double_4_extract_0(_read_temp8$2), double_4_extract_1(_read_temp8$2), double_4_extract_2(_read_temp8$2), double_4_extract_3(_read_temp8$2)) else f1234$2);
    _read_temp9$1, _read_temp9$2 := (if _P0$1 then construct_double_4.1_1_1_1(double_4_extract_2(f5678$1), double_4_extract_3(f5678$1), double_4_extract_0(f5678$1), double_4_extract_1(f5678$1)) else _read_temp9$1), (if _P0$2 then construct_double_4.1_1_1_1(double_4_extract_2(f5678$2), double_4_extract_3(f5678$2), double_4_extract_0(f5678$2), double_4_extract_1(f5678$2)) else _read_temp9$2);
    f5678$1, f5678$2 := (if _P0$1 then construct_double_4.1_1_1_1(double_4_extract_0(_read_temp9$1), double_4_extract_1(_read_temp9$1), double_4_extract_2(_read_temp9$1), double_4_extract_3(_read_temp9$1)) else f5678$1), (if _P0$2 then construct_double_4.1_1_1_1(double_4_extract_0(_read_temp9$2), double_4_extract_1(_read_temp9$2), double_4_extract_2(_read_temp9$2), double_4_extract_3(_read_temp9$2)) else f5678$2);
    rho$1, rho$2 := (if _P0$1 then bv32_to_double(0bv32) else rho$1), (if _P0$2 then bv32_to_double(0bv32) else rho$2);
    u$1, u$2 := (if _P0$1 then construct_double_2.1_1(bv32_to_double(0bv32), bv32_to_double(0bv32)) else u$1), (if _P0$2 then construct_double_2.1_1(bv32_to_double(0bv32), bv32_to_double(0bv32)) else u$2);

  anon120_Else:
    _read_temp10$1, _read_temp10$2 := (if !_P0$1 then f1234$1 else _read_temp10$1), (if !_P0$2 then f1234$2 else _read_temp10$2);
    _read_temp11$1, _read_temp11$2 := (if !_P0$1 then f5678$1 else _read_temp11$1), (if !_P0$2 then f5678$2 else _read_temp11$2);
    _read_temp12$1, _read_temp12$2 := (if !_P0$1 then f1234$1 else _read_temp12$1), (if !_P0$2 then f1234$2 else _read_temp12$2);
    _read_temp13$1, _read_temp13$2 := (if !_P0$1 then f5678$1 else _read_temp13$1), (if !_P0$2 then f5678$2 else _read_temp13$2);
    temp$1, temp$2 := (if !_P0$1 then construct_double_4.1_1_1_1(DOUBLE_ADD(double_4_extract_0(_read_temp12$1), double_4_extract_0(_read_temp13$1)), DOUBLE_ADD(double_4_extract_1(_read_temp12$1), double_4_extract_1(_read_temp13$1)), DOUBLE_ADD(double_4_extract_2(_read_temp12$1), double_4_extract_2(_read_temp13$1)), DOUBLE_ADD(double_4_extract_3(_read_temp12$1), double_4_extract_3(_read_temp13$1))) else temp$1), (if !_P0$2 then construct_double_4.1_1_1_1(DOUBLE_ADD(double_4_extract_0(_read_temp12$2), double_4_extract_0(_read_temp13$2)), DOUBLE_ADD(double_4_extract_1(_read_temp12$2), double_4_extract_1(_read_temp13$2)), DOUBLE_ADD(double_4_extract_2(_read_temp12$2), double_4_extract_2(_read_temp13$2)), DOUBLE_ADD(double_4_extract_3(_read_temp12$2), double_4_extract_3(_read_temp13$2))) else temp$2);
    _read_temp14$1, _read_temp14$2 := (if !_P0$1 then construct_double_2.1_1(double_4_extract_0(temp$1), double_4_extract_1(temp$1)) else _read_temp14$1), (if !_P0$2 then construct_double_2.1_1(double_4_extract_0(temp$2), double_4_extract_1(temp$2)) else _read_temp14$2);
    _read_temp15$1, _read_temp15$2 := (if !_P0$1 then construct_double_2.1_1(double_4_extract_2(temp$1), double_4_extract_3(temp$1)) else _read_temp15$1), (if !_P0$2 then construct_double_2.1_1(double_4_extract_2(temp$2), double_4_extract_3(temp$2)) else _read_temp15$2);
    _read_temp16$1, _read_temp16$2 := (if !_P0$1 then construct_double_2.1_1(DOUBLE_ADD(double_2_extract_0(_read_temp14$1), double_2_extract_0(_read_temp15$1)), DOUBLE_ADD(double_2_extract_1(_read_temp14$1), double_2_extract_1(_read_temp15$1))) else _read_temp16$1), (if !_P0$2 then construct_double_2.1_1(DOUBLE_ADD(double_2_extract_0(_read_temp14$2), double_2_extract_0(_read_temp15$2)), DOUBLE_ADD(double_2_extract_1(_read_temp14$2), double_2_extract_1(_read_temp15$2))) else _read_temp16$2);
    temp$1, temp$2 := (if !_P0$1 then construct_double_4.1_1_1_1(double_2_extract_0(_read_temp16$1), double_2_extract_1(_read_temp16$1), double_4_extract_2(temp$1), double_4_extract_3(temp$1)) else temp$1), (if !_P0$2 then construct_double_4.1_1_1_1(double_2_extract_0(_read_temp16$2), double_2_extract_1(_read_temp16$2), double_4_extract_2(temp$2), double_4_extract_3(temp$2)) else temp$2);
    rho$1, rho$2 := (if !_P0$1 then DOUBLE_ADD(double_4_extract_0(temp$1), double_4_extract_1(temp$1)) else rho$1), (if !_P0$2 then DOUBLE_ADD(double_4_extract_0(temp$2), double_4_extract_1(temp$2)) else rho$2);
    rho$1, rho$2 := (if !_P0$1 then DOUBLE_ADD(rho$1, f0$1) else rho$1), (if !_P0$2 then DOUBLE_ADD(rho$2, f0$2) else rho$2);
    _read_temp17$1, _read_temp17$2 := (if !_P0$1 then DOUBLE_DIV(DOUBLE_ADD(dot_double_4_double_4_double(f1234$1, construct_double_4.1_1_1_1(double_8_extract_0(dirX), double_8_extract_1(dirX), double_8_extract_2(dirX), double_8_extract_3(dirX))), dot_double_4_double_4_double(f5678$1, construct_double_4.1_1_1_1(double_8_extract_4(dirX), double_8_extract_5(dirX), double_8_extract_6(dirX), double_8_extract_7(dirX)))), rho$1) else _read_temp17$1), (if !_P0$2 then DOUBLE_DIV(DOUBLE_ADD(dot_double_4_double_4_double(f1234$2, construct_double_4.1_1_1_1(double_8_extract_0(dirX), double_8_extract_1(dirX), double_8_extract_2(dirX), double_8_extract_3(dirX))), dot_double_4_double_4_double(f5678$2, construct_double_4.1_1_1_1(double_8_extract_4(dirX), double_8_extract_5(dirX), double_8_extract_6(dirX), double_8_extract_7(dirX)))), rho$2) else _read_temp17$2);
    u$1, u$2 := (if !_P0$1 then construct_double_2.1_1(_read_temp17$1, double_2_extract_1(u$1)) else u$1), (if !_P0$2 then construct_double_2.1_1(_read_temp17$2, double_2_extract_1(u$2)) else u$2);
    _read_temp18$1, _read_temp18$2 := (if !_P0$1 then DOUBLE_DIV(DOUBLE_ADD(dot_double_4_double_4_double(f1234$1, construct_double_4.1_1_1_1(double_8_extract_0(dirY), double_8_extract_1(dirY), double_8_extract_2(dirY), double_8_extract_3(dirY))), dot_double_4_double_4_double(f5678$1, construct_double_4.1_1_1_1(double_8_extract_4(dirY), double_8_extract_5(dirY), double_8_extract_6(dirY), double_8_extract_7(dirY)))), rho$1) else _read_temp18$1), (if !_P0$2 then DOUBLE_DIV(DOUBLE_ADD(dot_double_4_double_4_double(f1234$2, construct_double_4.1_1_1_1(double_8_extract_0(dirY), double_8_extract_1(dirY), double_8_extract_2(dirY), double_8_extract_3(dirY))), dot_double_4_double_4_double(f5678$2, construct_double_4.1_1_1_1(double_8_extract_4(dirY), double_8_extract_5(dirY), double_8_extract_6(dirY), double_8_extract_7(dirY)))), rho$2) else _read_temp18$2);
    u$1, u$2 := (if !_P0$1 then construct_double_2.1_1(double_2_extract_0(u$1), _read_temp18$1) else u$1), (if !_P0$2 then construct_double_2.1_1(double_2_extract_0(u$2), _read_temp18$2) else u$2);
    _P1$1, _P1$2 := base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE, base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE;

  anon121_Then:
    _read_temp19$1, _read_temp19$2 := (if !_P0$1 && _P1$1 then _ARRAY_weight$1[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 0bv32)] else _read_temp19$1), (if !_P0$2 && _P1$2 then _ARRAY_weight$2[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 0bv32)] else _read_temp19$2);

  anon121_Else:
    assert (!_P0$1 && !_P1$1 ==> false) && (!_P0$2 && !_P1$2 ==> false);

  anon26:
    call _call_temp1$1, _call_temp1$2 := computefEq(construct_double_2.1_1(bv32_to_double(0bv32), bv32_to_double(0bv32)), !_P0$1, rho$1, _read_temp19$1, u$1, !_P0$2, rho$2, _read_temp19$2, u$2);
    fEq0$1, fEq0$2 := (if !_P0$1 then _call_temp1$1 else fEq0$1), (if !_P0$2 then _call_temp1$2 else fEq0$2);
    _P2$1, _P2$2 := base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE, base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE;

  anon122_Then:
    _read_temp20$1, _read_temp20$2 := (if !_P0$1 && _P2$1 then _ARRAY_weight$1[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 1bv32)] else _read_temp20$1), (if !_P0$2 && _P2$2 then _ARRAY_weight$2[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 1bv32)] else _read_temp20$2);

  anon122_Else:
    assert (!_P0$1 && !_P2$1 ==> false) && (!_P0$2 && !_P2$2 ==> false);

  anon29:
    call _call_temp2$1, _call_temp2$2 := computefEq(construct_double_2.1_1(double_8_extract_0(dirX), double_8_extract_0(dirY)), !_P0$1, rho$1, _read_temp20$1, u$1, !_P0$2, rho$2, _read_temp20$2, u$2);
    _read_temp21$1, _read_temp21$2 := (if !_P0$1 then _call_temp2$1 else _read_temp21$1), (if !_P0$2 then _call_temp2$2 else _read_temp21$2);
    fEq1234$1, fEq1234$2 := (if !_P0$1 then construct_double_4.1_1_1_1(_read_temp21$1, double_4_extract_1(fEq1234$1), double_4_extract_2(fEq1234$1), double_4_extract_3(fEq1234$1)) else fEq1234$1), (if !_P0$2 then construct_double_4.1_1_1_1(_read_temp21$2, double_4_extract_1(fEq1234$2), double_4_extract_2(fEq1234$2), double_4_extract_3(fEq1234$2)) else fEq1234$2);
    _P3$1, _P3$2 := base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE, base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE;

  anon123_Then:
    _read_temp22$1, _read_temp22$2 := (if !_P0$1 && _P3$1 then _ARRAY_weight$1[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 2bv32)] else _read_temp22$1), (if !_P0$2 && _P3$2 then _ARRAY_weight$2[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 2bv32)] else _read_temp22$2);

  anon123_Else:
    assert (!_P0$1 && !_P3$1 ==> false) && (!_P0$2 && !_P3$2 ==> false);

  anon32:
    call _call_temp3$1, _call_temp3$2 := computefEq(construct_double_2.1_1(double_8_extract_1(dirX), double_8_extract_1(dirY)), !_P0$1, rho$1, _read_temp22$1, u$1, !_P0$2, rho$2, _read_temp22$2, u$2);
    _read_temp23$1, _read_temp23$2 := (if !_P0$1 then _call_temp3$1 else _read_temp23$1), (if !_P0$2 then _call_temp3$2 else _read_temp23$2);
    fEq1234$1, fEq1234$2 := (if !_P0$1 then construct_double_4.1_1_1_1(double_4_extract_0(fEq1234$1), _read_temp23$1, double_4_extract_2(fEq1234$1), double_4_extract_3(fEq1234$1)) else fEq1234$1), (if !_P0$2 then construct_double_4.1_1_1_1(double_4_extract_0(fEq1234$2), _read_temp23$2, double_4_extract_2(fEq1234$2), double_4_extract_3(fEq1234$2)) else fEq1234$2);
    _P4$1, _P4$2 := base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE, base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE;

  anon124_Then:
    _read_temp24$1, _read_temp24$2 := (if !_P0$1 && _P4$1 then _ARRAY_weight$1[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 3bv32)] else _read_temp24$1), (if !_P0$2 && _P4$2 then _ARRAY_weight$2[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 3bv32)] else _read_temp24$2);

  anon124_Else:
    assert (!_P0$1 && !_P4$1 ==> false) && (!_P0$2 && !_P4$2 ==> false);

  anon35:
    call _call_temp4$1, _call_temp4$2 := computefEq(construct_double_2.1_1(double_8_extract_2(dirX), double_8_extract_2(dirY)), !_P0$1, rho$1, _read_temp24$1, u$1, !_P0$2, rho$2, _read_temp24$2, u$2);
    _read_temp25$1, _read_temp25$2 := (if !_P0$1 then _call_temp4$1 else _read_temp25$1), (if !_P0$2 then _call_temp4$2 else _read_temp25$2);
    fEq1234$1, fEq1234$2 := (if !_P0$1 then construct_double_4.1_1_1_1(double_4_extract_0(fEq1234$1), double_4_extract_1(fEq1234$1), _read_temp25$1, double_4_extract_3(fEq1234$1)) else fEq1234$1), (if !_P0$2 then construct_double_4.1_1_1_1(double_4_extract_0(fEq1234$2), double_4_extract_1(fEq1234$2), _read_temp25$2, double_4_extract_3(fEq1234$2)) else fEq1234$2);
    _P5$1, _P5$2 := base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE, base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE;

  anon125_Then:
    _read_temp26$1, _read_temp26$2 := (if !_P0$1 && _P5$1 then _ARRAY_weight$1[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 4bv32)] else _read_temp26$1), (if !_P0$2 && _P5$2 then _ARRAY_weight$2[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 4bv32)] else _read_temp26$2);

  anon125_Else:
    assert (!_P0$1 && !_P5$1 ==> false) && (!_P0$2 && !_P5$2 ==> false);

  anon38:
    call _call_temp5$1, _call_temp5$2 := computefEq(construct_double_2.1_1(double_8_extract_3(dirX), double_8_extract_3(dirY)), !_P0$1, rho$1, _read_temp26$1, u$1, !_P0$2, rho$2, _read_temp26$2, u$2);
    _read_temp27$1, _read_temp27$2 := (if !_P0$1 then _call_temp5$1 else _read_temp27$1), (if !_P0$2 then _call_temp5$2 else _read_temp27$2);
    fEq1234$1, fEq1234$2 := (if !_P0$1 then construct_double_4.1_1_1_1(double_4_extract_0(fEq1234$1), double_4_extract_1(fEq1234$1), double_4_extract_2(fEq1234$1), _read_temp27$1) else fEq1234$1), (if !_P0$2 then construct_double_4.1_1_1_1(double_4_extract_0(fEq1234$2), double_4_extract_1(fEq1234$2), double_4_extract_2(fEq1234$2), _read_temp27$2) else fEq1234$2);
    _P6$1, _P6$2 := base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE, base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE;

  anon126_Then:
    _read_temp28$1, _read_temp28$2 := (if !_P0$1 && _P6$1 then _ARRAY_weight$1[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 5bv32)] else _read_temp28$1), (if !_P0$2 && _P6$2 then _ARRAY_weight$2[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 5bv32)] else _read_temp28$2);

  anon126_Else:
    assert (!_P0$1 && !_P6$1 ==> false) && (!_P0$2 && !_P6$2 ==> false);

  anon41:
    call _call_temp6$1, _call_temp6$2 := computefEq(construct_double_2.1_1(double_8_extract_4(dirX), double_8_extract_4(dirY)), !_P0$1, rho$1, _read_temp28$1, u$1, !_P0$2, rho$2, _read_temp28$2, u$2);
    _read_temp29$1, _read_temp29$2 := (if !_P0$1 then _call_temp6$1 else _read_temp29$1), (if !_P0$2 then _call_temp6$2 else _read_temp29$2);
    fEq5678$1, fEq5678$2 := (if !_P0$1 then construct_double_4.1_1_1_1(_read_temp29$1, double_4_extract_1(fEq5678$1), double_4_extract_2(fEq5678$1), double_4_extract_3(fEq5678$1)) else fEq5678$1), (if !_P0$2 then construct_double_4.1_1_1_1(_read_temp29$2, double_4_extract_1(fEq5678$2), double_4_extract_2(fEq5678$2), double_4_extract_3(fEq5678$2)) else fEq5678$2);
    _P7$1, _P7$2 := base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE, base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE;

  anon127_Then:
    _read_temp30$1, _read_temp30$2 := (if !_P0$1 && _P7$1 then _ARRAY_weight$1[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 6bv32)] else _read_temp30$1), (if !_P0$2 && _P7$2 then _ARRAY_weight$2[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 6bv32)] else _read_temp30$2);

  anon127_Else:
    assert (!_P0$1 && !_P7$1 ==> false) && (!_P0$2 && !_P7$2 ==> false);

  anon44:
    call _call_temp7$1, _call_temp7$2 := computefEq(construct_double_2.1_1(double_8_extract_5(dirX), double_8_extract_5(dirY)), !_P0$1, rho$1, _read_temp30$1, u$1, !_P0$2, rho$2, _read_temp30$2, u$2);
    _read_temp31$1, _read_temp31$2 := (if !_P0$1 then _call_temp7$1 else _read_temp31$1), (if !_P0$2 then _call_temp7$2 else _read_temp31$2);
    fEq5678$1, fEq5678$2 := (if !_P0$1 then construct_double_4.1_1_1_1(double_4_extract_0(fEq5678$1), _read_temp31$1, double_4_extract_2(fEq5678$1), double_4_extract_3(fEq5678$1)) else fEq5678$1), (if !_P0$2 then construct_double_4.1_1_1_1(double_4_extract_0(fEq5678$2), _read_temp31$2, double_4_extract_2(fEq5678$2), double_4_extract_3(fEq5678$2)) else fEq5678$2);
    _P8$1, _P8$2 := base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE, base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE;

  anon128_Then:
    _read_temp32$1, _read_temp32$2 := (if !_P0$1 && _P8$1 then _ARRAY_weight$1[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 7bv32)] else _read_temp32$1), (if !_P0$2 && _P8$2 then _ARRAY_weight$2[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 7bv32)] else _read_temp32$2);

  anon128_Else:
    assert (!_P0$1 && !_P8$1 ==> false) && (!_P0$2 && !_P8$2 ==> false);

  anon47:
    call _call_temp8$1, _call_temp8$2 := computefEq(construct_double_2.1_1(double_8_extract_6(dirX), double_8_extract_6(dirY)), !_P0$1, rho$1, _read_temp32$1, u$1, !_P0$2, rho$2, _read_temp32$2, u$2);
    _read_temp33$1, _read_temp33$2 := (if !_P0$1 then _call_temp8$1 else _read_temp33$1), (if !_P0$2 then _call_temp8$2 else _read_temp33$2);
    fEq5678$1, fEq5678$2 := (if !_P0$1 then construct_double_4.1_1_1_1(double_4_extract_0(fEq5678$1), double_4_extract_1(fEq5678$1), _read_temp33$1, double_4_extract_3(fEq5678$1)) else fEq5678$1), (if !_P0$2 then construct_double_4.1_1_1_1(double_4_extract_0(fEq5678$2), double_4_extract_1(fEq5678$2), _read_temp33$2, double_4_extract_3(fEq5678$2)) else fEq5678$2);
    _P9$1, _P9$2 := base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE, base#_CONSTRUCT_POINTER_TO_constant_double(weight) == _ARRAY_weight_BASE;

  anon129_Then:
    _read_temp34$1, _read_temp34$2 := (if !_P0$1 && _P9$1 then _ARRAY_weight$1[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 8bv32)] else _read_temp34$1), (if !_P0$2 && _P9$2 then _ARRAY_weight$2[BV32_ADD(offset#_CONSTRUCT_POINTER_TO_constant_double(weight), 8bv32)] else _read_temp34$2);

  anon129_Else:
    assert (!_P0$1 && !_P9$1 ==> false) && (!_P0$2 && !_P9$2 ==> false);

  anon50:
    call _call_temp9$1, _call_temp9$2 := computefEq(construct_double_2.1_1(double_8_extract_7(dirX), double_8_extract_7(dirY)), !_P0$1, rho$1, _read_temp34$1, u$1, !_P0$2, rho$2, _read_temp34$2, u$2);
    _read_temp35$1, _read_temp35$2 := (if !_P0$1 then _call_temp9$1 else _read_temp35$1), (if !_P0$2 then _call_temp9$2 else _read_temp35$2);
    fEq5678$1, fEq5678$2 := (if !_P0$1 then construct_double_4.1_1_1_1(double_4_extract_0(fEq5678$1), double_4_extract_1(fEq5678$1), double_4_extract_2(fEq5678$1), _read_temp35$1) else fEq5678$1), (if !_P0$2 then construct_double_4.1_1_1_1(double_4_extract_0(fEq5678$2), double_4_extract_1(fEq5678$2), double_4_extract_2(fEq5678$2), _read_temp35$2) else fEq5678$2);
    f0$1, f0$2 := (if !_P0$1 then DOUBLE_ADD(DOUBLE_MUL(DOUBLE_SUB(bv32_to_double(1bv32), omega), f0$1), DOUBLE_MUL(omega, fEq0$1)) else f0$1), (if !_P0$2 then DOUBLE_ADD(DOUBLE_MUL(DOUBLE_SUB(bv32_to_double(1bv32), omega), f0$2), DOUBLE_MUL(omega, fEq0$2)) else f0$2);
    _read_temp36$1, _read_temp36$2 := (if !_P0$1 then construct_double_4.1_1_1_1(DOUBLE_SUB(bv32_to_double(1bv32), omega), DOUBLE_SUB(bv32_to_double(1bv32), omega), DOUBLE_SUB(bv32_to_double(1bv32), omega), DOUBLE_SUB(bv32_to_double(1bv32), omega)) else _read_temp36$1), (if !_P0$2 then construct_double_4.1_1_1_1(DOUBLE_SUB(bv32_to_double(1bv32), omega), DOUBLE_SUB(bv32_to_double(1bv32), omega), DOUBLE_SUB(bv32_to_double(1bv32), omega), DOUBLE_SUB(bv32_to_double(1bv32), omega)) else _read_temp36$2);
    _read_temp37$1, _read_temp37$2 := (if !_P0$1 then f1234$1 else _read_temp37$1), (if !_P0$2 then f1234$2 else _read_temp37$2);
    _read_temp40$1, _read_temp40$2 := (if !_P0$1 then construct_double_4.1_1_1_1(DOUBLE_MUL(double_4_extract_0(_read_temp36$1), double_4_extract_0(_read_temp37$1)), DOUBLE_MUL(double_4_extract_1(_read_temp36$1), double_4_extract_1(_read_temp37$1)), DOUBLE_MUL(double_4_extract_2(_read_temp36$1), double_4_extract_2(_read_temp37$1)), DOUBLE_MUL(double_4_extract_3(_read_temp36$1), double_4_extract_3(_read_temp37$1))) else _read_temp40$1), (if !_P0$2 then construct_double_4.1_1_1_1(DOUBLE_MUL(double_4_extract_0(_read_temp36$2), double_4_extract_0(_read_temp37$2)), DOUBLE_MUL(double_4_extract_1(_read_temp36$2), double_4_extract_1(_read_temp37$2)), DOUBLE_MUL(double_4_extract_2(_read_temp36$2), double_4_extract_2(_read_temp37$2)), DOUBLE_MUL(double_4_extract_3(_read_temp36$2), double_4_extract_3(_read_temp37$2))) else _read_temp40$2);
    _read_temp38$1, _read_temp38$2 := (if !_P0$1 then construct_double_4.1_1_1_1(omega, omega, omega, omega) else _read_temp38$1), (if !_P0$2 then construct_double_4.1_1_1_1(omega, omega, omega, omega) else _read_temp38$2);
    _read_temp39$1, _read_temp39$2 := (if !_P0$1 then fEq1234$1 else _read_temp39$1), (if !_P0$2 then fEq1234$2 else _read_temp39$2);
    _read_temp41$1, _read_temp41$2 := (if !_P0$1 then construct_double_4.1_1_1_1(DOUBLE_MUL(double_4_extract_0(_read_temp38$1), double_4_extract_0(_read_temp39$1)), DOUBLE_MUL(double_4_extract_1(_read_temp38$1), double_4_extract_1(_read_temp39$1)), DOUBLE_MUL(double_4_extract_2(_read_temp38$1), double_4_extract_2(_read_temp39$1)), DOUBLE_MUL(double_4_extract_3(_read_temp38$1), double_4_extract_3(_read_temp39$1))) else _read_temp41$1), (if !_P0$2 then construct_double_4.1_1_1_1(DOUBLE_MUL(double_4_extract_0(_read_temp38$2), double_4_extract_0(_read_temp39$2)), DOUBLE_MUL(double_4_extract_1(_read_temp38$2), double_4_extract_1(_read_temp39$2)), DOUBLE_MUL(double_4_extract_2(_read_temp38$2), double_4_extract_2(_read_temp39$2)), DOUBLE_MUL(double_4_extract_3(_read_temp38$2), double_4_extract_3(_read_temp39$2))) else _read_temp41$2);
    f1234$1, f1234$2 := (if !_P0$1 then construct_double_4.1_1_1_1(DOUBLE_ADD(double_4_extract_0(_read_temp40$1), double_4_extract_0(_read_temp41$1)), DOUBLE_ADD(double_4_extract_1(_read_temp40$1), double_4_extract_1(_read_temp41$1)), DOUBLE_ADD(double_4_extract_2(_read_temp40$1), double_4_extract_2(_read_temp41$1)), DOUBLE_ADD(double_4_extract_3(_read_temp40$1), double_4_extract_3(_read_temp41$1))) else f1234$1), (if !_P0$2 then construct_double_4.1_1_1_1(DOUBLE_ADD(double_4_extract_0(_read_temp40$2), double_4_extract_0(_read_temp41$2)), DOUBLE_ADD(double_4_extract_1(_read_temp40$2), double_4_extract_1(_read_temp41$2)), DOUBLE_ADD(double_4_extract_2(_read_temp40$2), double_4_extract_2(_read_temp41$2)), DOUBLE_ADD(double_4_extract_3(_read_temp40$2), double_4_extract_3(_read_temp41$2))) else f1234$2);
    _read_temp42$1, _read_temp42$2 := (if !_P0$1 then construct_double_4.1_1_1_1(DOUBLE_SUB(bv32_to_double(1bv32), omega), DOUBLE_SUB(bv32_to_double(1bv32), omega), DOUBLE_SUB(bv32_to_double(1bv32), omega), DOUBLE_SUB(bv32_to_double(1bv32), omega)) else _read_temp42$1), (if !_P0$2 then construct_double_4.1_1_1_1(DOUBLE_SUB(bv32_to_double(1bv32), omega), DOUBLE_SUB(bv32_to_double(1bv32), omega), DOUBLE_SUB(bv32_to_double(1bv32), omega), DOUBLE_SUB(bv32_to_double(1bv32), omega)) else _read_temp42$2);
    _read_temp43$1, _read_temp43$2 := (if !_P0$1 then f5678$1 else _read_temp43$1), (if !_P0$2 then f5678$2 else _read_temp43$2);
    _read_temp46$1, _read_temp46$2 := (if !_P0$1 then construct_double_4.1_1_1_1(DOUBLE_MUL(double_4_extract_0(_read_temp42$1), double_4_extract_0(_read_temp43$1)), DOUBLE_MUL(double_4_extract_1(_read_temp42$1), double_4_extract_1(_read_temp43$1)), DOUBLE_MUL(double_4_extract_2(_read_temp42$1), double_4_extract_2(_read_temp43$1)), DOUBLE_MUL(double_4_extract_3(_read_temp42$1), double_4_extract_3(_read_temp43$1))) else _read_temp46$1), (if !_P0$2 then construct_double_4.1_1_1_1(DOUBLE_MUL(double_4_extract_0(_read_temp42$2), double_4_extract_0(_read_temp43$2)), DOUBLE_MUL(double_4_extract_1(_read_temp42$2), double_4_extract_1(_read_temp43$2)), DOUBLE_MUL(double_4_extract_2(_read_temp42$2), double_4_extract_2(_read_temp43$2)), DOUBLE_MUL(double_4_extract_3(_read_temp42$2), double_4_extract_3(_read_temp43$2))) else _read_temp46$2);
    _read_temp44$1, _read_temp44$2 := (if !_P0$1 then construct_double_4.1_1_1_1(omega, omega, omega, omega) else _read_temp44$1), (if !_P0$2 then construct_double_4.1_1_1_1(omega, omega, omega, omega) else _read_temp44$2);
    _read_temp45$1, _read_temp45$2 := (if !_P0$1 then fEq5678$1 else _read_temp45$1), (if !_P0$2 then fEq5678$2 else _read_temp45$2);
    _read_temp47$1, _read_temp47$2 := (if !_P0$1 then construct_double_4.1_1_1_1(DOUBLE_MUL(double_4_extract_0(_read_temp44$1), double_4_extract_0(_read_temp45$1)), DOUBLE_MUL(double_4_extract_1(_read_temp44$1), double_4_extract_1(_read_temp45$1)), DOUBLE_MUL(double_4_extract_2(_read_temp44$1), double_4_extract_2(_read_temp45$1)), DOUBLE_MUL(double_4_extract_3(_read_temp44$1), double_4_extract_3(_read_temp45$1))) else _read_temp47$1), (if !_P0$2 then construct_double_4.1_1_1_1(DOUBLE_MUL(double_4_extract_0(_read_temp44$2), double_4_extract_0(_read_temp45$2)), DOUBLE_MUL(double_4_extract_1(_read_temp44$2), double_4_extract_1(_read_temp45$2)), DOUBLE_MUL(double_4_extract_2(_read_temp44$2), double_4_extract_2(_read_temp45$2)), DOUBLE_MUL(double_4_extract_3(_read_temp44$2), double_4_extract_3(_read_temp45$2))) else _read_temp47$2);
    f5678$1, f5678$2 := (if !_P0$1 then construct_double_4.1_1_1_1(DOUBLE_ADD(double_4_extract_0(_read_temp46$1), double_4_extract_0(_read_temp47$1)), DOUBLE_ADD(double_4_extract_1(_read_temp46$1), double_4_extract_1(_read_temp47$1)), DOUBLE_ADD(double_4_extract_2(_read_temp46$1), double_4_extract_2(_read_temp47$1)), DOUBLE_ADD(double_4_extract_3(_read_temp46$1), double_4_extract_3(_read_temp47$1))) else f5678$1), (if !_P0$2 then construct_double_4.1_1_1_1(DOUBLE_ADD(double_4_extract_0(_read_temp46$2), double_4_extract_0(_read_temp47$2)), DOUBLE_ADD(double_4_extract_1(_read_temp46$2), double_4_extract_1(_read_temp47$2)), DOUBLE_ADD(double_4_extract_2(_read_temp46$2), double_4_extract_2(_read_temp47$2)), DOUBLE_ADD(double_4_extract_3(_read_temp46$2), double_4_extract_3(_read_temp47$2))) else f5678$2);

  anon51:
    if (base#_CONSTRUCT_POINTER_TO_global_double_2(velocityBuffer) == _ARRAY_velocityBuffer_BASE)
    {
      anon130_Then:
        call _LOG_WRITE__ARRAY_velocityBuffer(true, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_2(velocityBuffer), pos$1), true, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_2(velocityBuffer), pos$2));
    }
    else
    {
      anon130_Else:
        assert false && false;
    }

  anon54:
    _read_temp48$1, _read_temp48$2 := construct_bv32_8.1_1_1_1_1_1_1_1(bv32_2_extract_0(id$1), bv32_2_extract_0(id$1), bv32_2_extract_0(id$1), bv32_2_extract_0(id$1), bv32_2_extract_0(id$1), bv32_2_extract_0(id$1), bv32_2_extract_0(id$1), bv32_2_extract_0(id$1)), construct_bv32_8.1_1_1_1_1_1_1_1(bv32_2_extract_0(id$2), bv32_2_extract_0(id$2), bv32_2_extract_0(id$2), bv32_2_extract_0(id$2), bv32_2_extract_0(id$2), bv32_2_extract_0(id$2), bv32_2_extract_0(id$2), bv32_2_extract_0(id$2));

    // Ally question: why is this line generated?  The read temp is never used
    _read_temp49 := convert_int8_double_8_bv32_8(dirX);

    _read_temp50$1, _read_temp50$2 := construct_bv32_8.1_1_1_1_1_1_1_1(bv32_2_extract_0(id$1), bv32_2_extract_0(id$1), bv32_2_extract_0(id$1), bv32_2_extract_0(id$1), bv32_2_extract_0(id$1), bv32_2_extract_0(id$1), bv32_2_extract_0(id$1), bv32_2_extract_0(id$1)), construct_bv32_8.1_1_1_1_1_1_1_1(bv32_2_extract_0(id$2), bv32_2_extract_0(id$2), bv32_2_extract_0(id$2), bv32_2_extract_0(id$2), bv32_2_extract_0(id$2), bv32_2_extract_0(id$2), bv32_2_extract_0(id$2), bv32_2_extract_0(id$2));

    _read_temp51 := convert_int8_double_8_bv32_8(dirX);

    // Ally added:
    _read_temp51 := construct_bv32_8.1_1_1_1_1_1_1_1(0bv32, 1bv32, 2bv32, 3bv32, 4bv32, 5bv32, 6bv32, 7bv32);

    nX$1, nX$2 := construct_bv32_8.1_1_1_1_1_1_1_1(BV32_ADD(bv32_8_extract_0(_read_temp50$1), bv32_8_extract_0(_read_temp51)), BV32_ADD(bv32_8_extract_1(_read_temp50$1), bv32_8_extract_1(_read_temp51)), BV32_ADD(bv32_8_extract_2(_read_temp50$1), bv32_8_extract_2(_read_temp51)), BV32_ADD(bv32_8_extract_3(_read_temp50$1), bv32_8_extract_3(_read_temp51)), BV32_ADD(bv32_8_extract_4(_read_temp50$1), bv32_8_extract_4(_read_temp51)), BV32_ADD(bv32_8_extract_5(_read_temp50$1), bv32_8_extract_5(_read_temp51)), BV32_ADD(bv32_8_extract_6(_read_temp50$1), bv32_8_extract_6(_read_temp51)), BV32_ADD(bv32_8_extract_7(_read_temp50$1), bv32_8_extract_7(_read_temp51))), construct_bv32_8.1_1_1_1_1_1_1_1(BV32_ADD(bv32_8_extract_0(_read_temp50$2), bv32_8_extract_0(_read_temp51)), BV32_ADD(bv32_8_extract_1(_read_temp50$2), bv32_8_extract_1(_read_temp51)), BV32_ADD(bv32_8_extract_2(_read_temp50$2), bv32_8_extract_2(_read_temp51)), BV32_ADD(bv32_8_extract_3(_read_temp50$2), bv32_8_extract_3(_read_temp51)), BV32_ADD(bv32_8_extract_4(_read_temp50$2), bv32_8_extract_4(_read_temp51)), BV32_ADD(bv32_8_extract_5(_read_temp50$2), bv32_8_extract_5(_read_temp51)), BV32_ADD(bv32_8_extract_6(_read_temp50$2), bv32_8_extract_6(_read_temp51)), BV32_ADD(bv32_8_extract_7(_read_temp50$2), bv32_8_extract_7(_read_temp51)));
    _read_temp52$1, _read_temp52$2 := construct_bv32_8.1_1_1_1_1_1_1_1(bv32_2_extract_1(id$1), bv32_2_extract_1(id$1), bv32_2_extract_1(id$1), bv32_2_extract_1(id$1), bv32_2_extract_1(id$1), bv32_2_extract_1(id$1), bv32_2_extract_1(id$1), bv32_2_extract_1(id$1)), construct_bv32_8.1_1_1_1_1_1_1_1(bv32_2_extract_1(id$2), bv32_2_extract_1(id$2), bv32_2_extract_1(id$2), bv32_2_extract_1(id$2), bv32_2_extract_1(id$2), bv32_2_extract_1(id$2), bv32_2_extract_1(id$2), bv32_2_extract_1(id$2));

    // Ally question: why is this line generated?  The read temp is never used
    _read_temp53 := convert_int8_double_8_bv32_8(dirY);

    _read_temp54$1, _read_temp54$2 := construct_bv32_8.1_1_1_1_1_1_1_1(bv32_2_extract_1(id$1), bv32_2_extract_1(id$1), bv32_2_extract_1(id$1), bv32_2_extract_1(id$1), bv32_2_extract_1(id$1), bv32_2_extract_1(id$1), bv32_2_extract_1(id$1), bv32_2_extract_1(id$1)), construct_bv32_8.1_1_1_1_1_1_1_1(bv32_2_extract_1(id$2), bv32_2_extract_1(id$2), bv32_2_extract_1(id$2), bv32_2_extract_1(id$2), bv32_2_extract_1(id$2), bv32_2_extract_1(id$2), bv32_2_extract_1(id$2), bv32_2_extract_1(id$2));
    _read_temp55 := convert_int8_double_8_bv32_8(dirY);

    // Ally added:
    _read_temp55 := construct_bv32_8.1_1_1_1_1_1_1_1(0bv32, 1bv32, 2bv32, 3bv32, 4bv32, 5bv32, 6bv32, 7bv32);

    nY$1, nY$2 := construct_bv32_8.1_1_1_1_1_1_1_1(BV32_ADD(bv32_8_extract_0(_read_temp54$1), bv32_8_extract_0(_read_temp55)), BV32_ADD(bv32_8_extract_1(_read_temp54$1), bv32_8_extract_1(_read_temp55)), BV32_ADD(bv32_8_extract_2(_read_temp54$1), bv32_8_extract_2(_read_temp55)), BV32_ADD(bv32_8_extract_3(_read_temp54$1), bv32_8_extract_3(_read_temp55)), BV32_ADD(bv32_8_extract_4(_read_temp54$1), bv32_8_extract_4(_read_temp55)), BV32_ADD(bv32_8_extract_5(_read_temp54$1), bv32_8_extract_5(_read_temp55)), BV32_ADD(bv32_8_extract_6(_read_temp54$1), bv32_8_extract_6(_read_temp55)), BV32_ADD(bv32_8_extract_7(_read_temp54$1), bv32_8_extract_7(_read_temp55))), construct_bv32_8.1_1_1_1_1_1_1_1(BV32_ADD(bv32_8_extract_0(_read_temp54$2), bv32_8_extract_0(_read_temp55)), BV32_ADD(bv32_8_extract_1(_read_temp54$2), bv32_8_extract_1(_read_temp55)), BV32_ADD(bv32_8_extract_2(_read_temp54$2), bv32_8_extract_2(_read_temp55)), BV32_ADD(bv32_8_extract_3(_read_temp54$2), bv32_8_extract_3(_read_temp55)), BV32_ADD(bv32_8_extract_4(_read_temp54$2), bv32_8_extract_4(_read_temp55)), BV32_ADD(bv32_8_extract_5(_read_temp54$2), bv32_8_extract_5(_read_temp55)), BV32_ADD(bv32_8_extract_6(_read_temp54$2), bv32_8_extract_6(_read_temp55)), BV32_ADD(bv32_8_extract_7(_read_temp54$2), bv32_8_extract_7(_read_temp55)));
    _read_temp58$1, _read_temp58$2 := nX$1, nX$2;
    _read_temp56 := construct_bv32_8.1_1_1_1_1_1_1_1(width, width, width, width, width, width, width, width);
    _read_temp57$1, _read_temp57$2 := nY$1, nY$2;
    _read_temp59$1, _read_temp59$2 := construct_bv32_8.1_1_1_1_1_1_1_1(BV32_MUL(bv32_8_extract_0(_read_temp56), bv32_8_extract_0(_read_temp57$1)), BV32_MUL(bv32_8_extract_1(_read_temp56), bv32_8_extract_1(_read_temp57$1)), BV32_MUL(bv32_8_extract_2(_read_temp56), bv32_8_extract_2(_read_temp57$1)), BV32_MUL(bv32_8_extract_3(_read_temp56), bv32_8_extract_3(_read_temp57$1)), BV32_MUL(bv32_8_extract_4(_read_temp56), bv32_8_extract_4(_read_temp57$1)), BV32_MUL(bv32_8_extract_5(_read_temp56), bv32_8_extract_5(_read_temp57$1)), BV32_MUL(bv32_8_extract_6(_read_temp56), bv32_8_extract_6(_read_temp57$1)), BV32_MUL(bv32_8_extract_7(_read_temp56), bv32_8_extract_7(_read_temp57$1))), construct_bv32_8.1_1_1_1_1_1_1_1(BV32_MUL(bv32_8_extract_0(_read_temp56), bv32_8_extract_0(_read_temp57$2)), BV32_MUL(bv32_8_extract_1(_read_temp56), bv32_8_extract_1(_read_temp57$2)), BV32_MUL(bv32_8_extract_2(_read_temp56), bv32_8_extract_2(_read_temp57$2)), BV32_MUL(bv32_8_extract_3(_read_temp56), bv32_8_extract_3(_read_temp57$2)), BV32_MUL(bv32_8_extract_4(_read_temp56), bv32_8_extract_4(_read_temp57$2)), BV32_MUL(bv32_8_extract_5(_read_temp56), bv32_8_extract_5(_read_temp57$2)), BV32_MUL(bv32_8_extract_6(_read_temp56), bv32_8_extract_6(_read_temp57$2)), BV32_MUL(bv32_8_extract_7(_read_temp56), bv32_8_extract_7(_read_temp57$2)));
    _read_temp62$1, _read_temp62$2 := nX$1, nX$2;
    _read_temp60 := construct_bv32_8.1_1_1_1_1_1_1_1(width, width, width, width, width, width, width, width);
    _read_temp61$1, _read_temp61$2 := nY$1, nY$2;
    _read_temp63$1, _read_temp63$2 := construct_bv32_8.1_1_1_1_1_1_1_1(BV32_MUL(bv32_8_extract_0(_read_temp60), bv32_8_extract_0(_read_temp61$1)), BV32_MUL(bv32_8_extract_1(_read_temp60), bv32_8_extract_1(_read_temp61$1)), BV32_MUL(bv32_8_extract_2(_read_temp60), bv32_8_extract_2(_read_temp61$1)), BV32_MUL(bv32_8_extract_3(_read_temp60), bv32_8_extract_3(_read_temp61$1)), BV32_MUL(bv32_8_extract_4(_read_temp60), bv32_8_extract_4(_read_temp61$1)), BV32_MUL(bv32_8_extract_5(_read_temp60), bv32_8_extract_5(_read_temp61$1)), BV32_MUL(bv32_8_extract_6(_read_temp60), bv32_8_extract_6(_read_temp61$1)), BV32_MUL(bv32_8_extract_7(_read_temp60), bv32_8_extract_7(_read_temp61$1))), construct_bv32_8.1_1_1_1_1_1_1_1(BV32_MUL(bv32_8_extract_0(_read_temp60), bv32_8_extract_0(_read_temp61$2)), BV32_MUL(bv32_8_extract_1(_read_temp60), bv32_8_extract_1(_read_temp61$2)), BV32_MUL(bv32_8_extract_2(_read_temp60), bv32_8_extract_2(_read_temp61$2)), BV32_MUL(bv32_8_extract_3(_read_temp60), bv32_8_extract_3(_read_temp61$2)), BV32_MUL(bv32_8_extract_4(_read_temp60), bv32_8_extract_4(_read_temp61$2)), BV32_MUL(bv32_8_extract_5(_read_temp60), bv32_8_extract_5(_read_temp61$2)), BV32_MUL(bv32_8_extract_6(_read_temp60), bv32_8_extract_6(_read_temp61$2)), BV32_MUL(bv32_8_extract_7(_read_temp60), bv32_8_extract_7(_read_temp61$2)));
    nPos$1, nPos$2 := construct_bv32_8.1_1_1_1_1_1_1_1(BV32_ADD(bv32_8_extract_0(_read_temp62$1), bv32_8_extract_0(_read_temp63$1)), BV32_ADD(bv32_8_extract_1(_read_temp62$1), bv32_8_extract_1(_read_temp63$1)), BV32_ADD(bv32_8_extract_2(_read_temp62$1), bv32_8_extract_2(_read_temp63$1)), BV32_ADD(bv32_8_extract_3(_read_temp62$1), bv32_8_extract_3(_read_temp63$1)), BV32_ADD(bv32_8_extract_4(_read_temp62$1), bv32_8_extract_4(_read_temp63$1)), BV32_ADD(bv32_8_extract_5(_read_temp62$1), bv32_8_extract_5(_read_temp63$1)), BV32_ADD(bv32_8_extract_6(_read_temp62$1), bv32_8_extract_6(_read_temp63$1)), BV32_ADD(bv32_8_extract_7(_read_temp62$1), bv32_8_extract_7(_read_temp63$1))), construct_bv32_8.1_1_1_1_1_1_1_1(BV32_ADD(bv32_8_extract_0(_read_temp62$2), bv32_8_extract_0(_read_temp63$2)), BV32_ADD(bv32_8_extract_1(_read_temp62$2), bv32_8_extract_1(_read_temp63$2)), BV32_ADD(bv32_8_extract_2(_read_temp62$2), bv32_8_extract_2(_read_temp63$2)), BV32_ADD(bv32_8_extract_3(_read_temp62$2), bv32_8_extract_3(_read_temp63$2)), BV32_ADD(bv32_8_extract_4(_read_temp62$2), bv32_8_extract_4(_read_temp63$2)), BV32_ADD(bv32_8_extract_5(_read_temp62$2), bv32_8_extract_5(_read_temp63$2)), BV32_ADD(bv32_8_extract_6(_read_temp62$2), bv32_8_extract_6(_read_temp63$2)), BV32_ADD(bv32_8_extract_7(_read_temp62$2), bv32_8_extract_7(_read_temp63$2)));
    if (base#_CONSTRUCT_POINTER_TO_global_double(of0) == _ARRAY_of0_BASE)
    {
      anon131_Then:
        call _LOG_WRITE__ARRAY_of0(true, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double(of0), pos$1), true, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double(of0), pos$2));
    }
    else
    {
      anon131_Else:
        assert false && false;
    }

  anon57:
    t1$1, t1$2 := BV32_C_LT(bv32_2_extract_0(id$1), BV32_SUB(BV32_MUL(get_local_size.0, get_num_groups.0), 1bv32)), BV32_C_LT(bv32_2_extract_0(id$2), BV32_SUB(BV32_MUL(get_local_size.0, get_num_groups.0), 1bv32));
    t4$1, t4$2 := BV32_C_GT(bv32_2_extract_1(id$1), 0bv32), BV32_C_GT(bv32_2_extract_1(id$2), 0bv32);
    t3$1, t3$2 := BV32_C_GT(bv32_2_extract_0(id$1), 0bv32), BV32_C_GT(bv32_2_extract_0(id$2), 0bv32);
    t2$1, t2$2 := BV32_C_LT(bv32_2_extract_1(id$1), BV32_SUB(BV32_MUL(get_local_size.1, get_num_groups.1), 1bv32)), BV32_C_LT(bv32_2_extract_1(id$2), BV32_SUB(BV32_MUL(get_local_size.1, get_num_groups.1), 1bv32));
    _P10$1, _P10$2 := bv32_to_bool(t1$1), bv32_to_bool(t1$2);

  anon132_Then:
    _P11$1, _P11$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE;

  anon133_Then:
    havoc _HAVOC_double_4$1, _HAVOC_double_4$2;
    _read_temp64$1, _read_temp64$2 := (if _P10$1 && _P11$1 then _HAVOC_double_4$1 else _read_temp64$1), (if _P10$2 && _P11$2 then _HAVOC_double_4$2 else _read_temp64$2);
    call _LOG_READ__ARRAY_of1234(_P10$1 && _P11$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of1234), bv32_8_extract_0(nPos$1)));

  anon133_Else:
    assert (_P10$1 && !_P11$1 ==> false) && (_P10$2 && !_P11$2 ==> false);

  anon61:
    _read_temp65$1, _read_temp65$2 := (if _P10$1 then double_4_extract_0(f1234$1) else _read_temp65$1), (if _P10$2 then double_4_extract_0(f1234$2) else _read_temp65$2);
    _P12$1, _P12$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE;

  anon134_Then:
    call _LOG_WRITE__ARRAY_of1234(_P10$1 && _P12$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of1234), bv32_8_extract_0(nPos$1)), _P10$2 && _P12$2, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of1234), bv32_8_extract_0(nPos$2)));

  anon134_Else:
    assert (_P10$1 && !_P12$1 ==> false) && (_P10$2 && !_P12$2 ==> false);

  anon64:
    _P13$1, _P13$2 := bv32_to_bool(t2$1), bv32_to_bool(t2$2);

  anon135_Then:
    _P14$1, _P14$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE;

  anon136_Then:
    havoc _HAVOC_double_4$1, _HAVOC_double_4$2;
    _read_temp66$1, _read_temp66$2 := (if _P13$1 && _P14$1 then _HAVOC_double_4$1 else _read_temp66$1), (if _P13$2 && _P14$2 then _HAVOC_double_4$2 else _read_temp66$2);
    call _LOG_READ__ARRAY_of1234(_P13$1 && _P14$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of1234), bv32_8_extract_1(nPos$1)));

  anon136_Else:
    assert (_P13$1 && !_P14$1 ==> false) && (_P13$2 && !_P14$2 ==> false);

  anon68:
    _read_temp67$1, _read_temp67$2 := (if _P13$1 then double_4_extract_1(f1234$1) else _read_temp67$1), (if _P13$2 then double_4_extract_1(f1234$2) else _read_temp67$2);
    _P15$1, _P15$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE;

  anon137_Then:
    call _LOG_WRITE__ARRAY_of1234(_P13$1 && _P15$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of1234), bv32_8_extract_1(nPos$1)), _P13$2 && _P15$2, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of1234), bv32_8_extract_1(nPos$2)));

  anon137_Else:
    assert (_P13$1 && !_P15$1 ==> false) && (_P13$2 && !_P15$2 ==> false);

  anon71:
    _P16$1, _P16$2 := bv32_to_bool(t3$1), bv32_to_bool(t3$2);

  anon138_Then:
    _P17$1, _P17$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE;

  anon139_Then:
    havoc _HAVOC_double_4$1, _HAVOC_double_4$2;
    _read_temp68$1, _read_temp68$2 := (if _P16$1 && _P17$1 then _HAVOC_double_4$1 else _read_temp68$1), (if _P16$2 && _P17$2 then _HAVOC_double_4$2 else _read_temp68$2);
    call _LOG_READ__ARRAY_of1234(_P16$1 && _P17$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of1234), bv32_8_extract_2(nPos$1)));

  anon139_Else:
    assert (_P16$1 && !_P17$1 ==> false) && (_P16$2 && !_P17$2 ==> false);

  anon75:
    _read_temp69$1, _read_temp69$2 := (if _P16$1 then double_4_extract_2(f1234$1) else _read_temp69$1), (if _P16$2 then double_4_extract_2(f1234$2) else _read_temp69$2);
    _P18$1, _P18$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE;

  anon140_Then:
    call _LOG_WRITE__ARRAY_of1234(_P16$1 && _P18$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of1234), bv32_8_extract_2(nPos$1)), _P16$2 && _P18$2, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of1234), bv32_8_extract_2(nPos$2)));

  anon140_Else:
    assert (_P16$1 && !_P18$1 ==> false) && (_P16$2 && !_P18$2 ==> false);

  anon78:
    _P19$1, _P19$2 := bv32_to_bool(t4$1), bv32_to_bool(t4$2);

  anon141_Then:
    _P20$1, _P20$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE;

  anon142_Then:
    havoc _HAVOC_double_4$1, _HAVOC_double_4$2;
    _read_temp70$1, _read_temp70$2 := (if _P19$1 && _P20$1 then _HAVOC_double_4$1 else _read_temp70$1), (if _P19$2 && _P20$2 then _HAVOC_double_4$2 else _read_temp70$2);
    call _LOG_READ__ARRAY_of1234(_P19$1 && _P20$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of1234), bv32_8_extract_3(nPos$1)));

  anon142_Else:
    assert (_P19$1 && !_P20$1 ==> false) && (_P19$2 && !_P20$2 ==> false);

  anon82:
    _read_temp71$1, _read_temp71$2 := (if _P19$1 then double_4_extract_3(f1234$1) else _read_temp71$1), (if _P19$2 then double_4_extract_3(f1234$2) else _read_temp71$2);
    _P21$1, _P21$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of1234) == _ARRAY_of1234_BASE;

  anon143_Then:
    call _LOG_WRITE__ARRAY_of1234(_P19$1 && _P21$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of1234), bv32_8_extract_3(nPos$1)), _P19$2 && _P21$2, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of1234), bv32_8_extract_3(nPos$2)));

  anon143_Else:
    assert (_P19$1 && !_P21$1 ==> false) && (_P19$2 && !_P21$2 ==> false);

  anon85:
    _P22$1, _P22$2 := bv32_to_bool(BV32_C_LAND(t1$1, t2$1)), bv32_to_bool(BV32_C_LAND(t1$2, t2$2));

  anon144_Then:
    _P23$1, _P23$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE;

  anon145_Then:
    havoc _HAVOC_double_4$1, _HAVOC_double_4$2;
    _read_temp72$1, _read_temp72$2 := (if _P22$1 && _P23$1 then _HAVOC_double_4$1 else _read_temp72$1), (if _P22$2 && _P23$2 then _HAVOC_double_4$2 else _read_temp72$2);
    call _LOG_READ__ARRAY_of5678(_P22$1 && _P23$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of5678), bv32_8_extract_4(nPos$1)));

  anon145_Else:
    assert (_P22$1 && !_P23$1 ==> false) && (_P22$2 && !_P23$2 ==> false);

  anon89:
    _read_temp73$1, _read_temp73$2 := (if _P22$1 then double_4_extract_0(f5678$1) else _read_temp73$1), (if _P22$2 then double_4_extract_0(f5678$2) else _read_temp73$2);
    _P24$1, _P24$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE;

  anon146_Then:
    call _LOG_WRITE__ARRAY_of5678(_P22$1 && _P24$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of5678), bv32_8_extract_4(nPos$1)), _P22$2 && _P24$2, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of5678), bv32_8_extract_4(nPos$2)));

  anon146_Else:
    assert (_P22$1 && !_P24$1 ==> false) && (_P22$2 && !_P24$2 ==> false);

  anon92:
    _P25$1, _P25$2 := bv32_to_bool(BV32_C_LAND(t2$1, t3$1)), bv32_to_bool(BV32_C_LAND(t2$2, t3$2));

  anon147_Then:
    _P26$1, _P26$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE;

  anon148_Then:
    havoc _HAVOC_double_4$1, _HAVOC_double_4$2;
    _read_temp74$1, _read_temp74$2 := (if _P25$1 && _P26$1 then _HAVOC_double_4$1 else _read_temp74$1), (if _P25$2 && _P26$2 then _HAVOC_double_4$2 else _read_temp74$2);
    call _LOG_READ__ARRAY_of5678(_P25$1 && _P26$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of5678), bv32_8_extract_5(nPos$1)));

  anon148_Else:
    assert (_P25$1 && !_P26$1 ==> false) && (_P25$2 && !_P26$2 ==> false);

  anon96:
    _read_temp75$1, _read_temp75$2 := (if _P25$1 then double_4_extract_1(f5678$1) else _read_temp75$1), (if _P25$2 then double_4_extract_1(f5678$2) else _read_temp75$2);
    _P27$1, _P27$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE;

  anon149_Then:
    call _LOG_WRITE__ARRAY_of5678(_P25$1 && _P27$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of5678), bv32_8_extract_5(nPos$1)), _P25$2 && _P27$2, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of5678), bv32_8_extract_5(nPos$2)));

  anon149_Else:
    assert (_P25$1 && !_P27$1 ==> false) && (_P25$2 && !_P27$2 ==> false);

  anon99:
    _P28$1, _P28$2 := bv32_to_bool(BV32_C_LAND(t3$1, t4$1)), bv32_to_bool(BV32_C_LAND(t3$2, t4$2));

  anon150_Then:
    _P29$1, _P29$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE;

  anon151_Then:
    havoc _HAVOC_double_4$1, _HAVOC_double_4$2;
    _read_temp76$1, _read_temp76$2 := (if _P28$1 && _P29$1 then _HAVOC_double_4$1 else _read_temp76$1), (if _P28$2 && _P29$2 then _HAVOC_double_4$2 else _read_temp76$2);
    call _LOG_READ__ARRAY_of5678(_P28$1 && _P29$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of5678), bv32_8_extract_6(nPos$1)));

  anon151_Else:
    assert (_P28$1 && !_P29$1 ==> false) && (_P28$2 && !_P29$2 ==> false);

  anon103:
    _read_temp77$1, _read_temp77$2 := (if _P28$1 then double_4_extract_2(f5678$1) else _read_temp77$1), (if _P28$2 then double_4_extract_2(f5678$2) else _read_temp77$2);
    _P30$1, _P30$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE;

  anon152_Then:
    call _LOG_WRITE__ARRAY_of5678(_P28$1 && _P30$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of5678), bv32_8_extract_6(nPos$1)), _P28$2 && _P30$2, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of5678), bv32_8_extract_6(nPos$2)));

  anon152_Else:
    assert (_P28$1 && !_P30$1 ==> false) && (_P28$2 && !_P30$2 ==> false);

  anon106:
    _P31$1, _P31$2 := bv32_to_bool(BV32_C_LAND(t4$1, t1$1)), bv32_to_bool(BV32_C_LAND(t4$2, t1$2));

  anon153_Then:
    _P32$1, _P32$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE;

  anon154_Then:
    havoc _HAVOC_double_4$1, _HAVOC_double_4$2;
    _read_temp78$1, _read_temp78$2 := (if _P31$1 && _P32$1 then _HAVOC_double_4$1 else _read_temp78$1), (if _P31$2 && _P32$2 then _HAVOC_double_4$2 else _read_temp78$2);
    call _LOG_READ__ARRAY_of5678(_P31$1 && _P32$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of5678), bv32_8_extract_7(nPos$1)));

  anon154_Else:
    assert (_P31$1 && !_P32$1 ==> false) && (_P31$2 && !_P32$2 ==> false);

  anon110:
    _read_temp79$1, _read_temp79$2 := (if _P31$1 then double_4_extract_3(f5678$1) else _read_temp79$1), (if _P31$2 then double_4_extract_3(f5678$2) else _read_temp79$2);
    _P33$1, _P33$2 := base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE, base#_CONSTRUCT_POINTER_TO_global_double_4(of5678) == _ARRAY_of5678_BASE;

  anon155_Then:
    call _LOG_WRITE__ARRAY_of5678(_P31$1 && _P33$1, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of5678), bv32_8_extract_7(nPos$1)), _P31$2 && _P33$2, BV32_ADD(offset#_CONSTRUCT_POINTER_TO_global_double_4(of5678), bv32_8_extract_7(nPos$2)));

  anon155_Else:
    assert (_P31$1 && !_P33$1 ==> false) && (_P31$2 && !_P33$2 ==> false);
}



procedure computefEq(_param_dir: double_2, _P$1: bool, _param_rho$1: double, _param_weight$1: double, _param_u$1: double_2, _P$2: bool, _param_rho$2: double, _param_weight$2: double, _param_u$2: double_2) returns (_returnVal$1: double, _returnVal$2: double);
  requires BV32_GT(get_local_size.0, 0bv32);
  requires BV32_GT(get_num_groups.0, 0bv32);
  requires BV32_GEQ(get_group_id.0, 0bv32);
  requires BV32_LT(get_group_id.0, get_num_groups.0);
  requires BV32_GT(get_local_size.1, 0bv32);
  requires BV32_GT(get_num_groups.1, 0bv32);
  requires BV32_GEQ(get_group_id.1, 0bv32);
  requires BV32_LT(get_group_id.1, get_num_groups.1);
  requires BV32_GT(get_local_size.2, 0bv32);
  requires BV32_GT(get_num_groups.2, 0bv32);
  requires BV32_GEQ(get_group_id.2, 0bv32);
  requires BV32_LT(get_group_id.2, get_num_groups.2);
  requires get_local_id.0$1 != get_local_id.0$2 || get_local_id.1$1 != get_local_id.1$2 || get_local_id.2$1 != get_local_id.2$2;
  requires BV32_GEQ(get_local_id.0$1, 0bv32) && BV32_GEQ(get_local_id.0$2, 0bv32) && BV32_LT(get_local_id.0$1, get_local_size.0) && BV32_LT(get_local_id.0$2, get_local_size.0) && BV32_GEQ(get_local_id.1$1, 0bv32) && BV32_GEQ(get_local_id.1$2, 0bv32) && BV32_LT(get_local_id.1$1, get_local_size.1) && BV32_LT(get_local_id.1$2, get_local_size.1) && BV32_GEQ(get_local_id.2$1, 0bv32) && BV32_GEQ(get_local_id.2$2, 0bv32) && BV32_LT(get_local_id.2$1, get_local_size.2) && BV32_LT(get_local_id.2$2, get_local_size.2);
  requires !(_WRITE_HAS_OCCURRED__ARRAY_if0$1 && _WRITE_HAS_OCCURRED__ARRAY_if0$2 && _WRITE_OFFSET_X__ARRAY_if0$1 == _WRITE_OFFSET_X__ARRAY_if0$2);
  requires !(_READ_HAS_OCCURRED__ARRAY_if0$1 && _WRITE_HAS_OCCURRED__ARRAY_if0$2 && _READ_OFFSET_X__ARRAY_if0$1 == _WRITE_OFFSET_X__ARRAY_if0$2);
  requires !(_WRITE_HAS_OCCURRED__ARRAY_of0$1 && _WRITE_HAS_OCCURRED__ARRAY_of0$2 && _WRITE_OFFSET_X__ARRAY_of0$1 == _WRITE_OFFSET_X__ARRAY_of0$2);
  requires !(_READ_HAS_OCCURRED__ARRAY_of0$1 && _WRITE_HAS_OCCURRED__ARRAY_of0$2 && _READ_OFFSET_X__ARRAY_of0$1 == _WRITE_OFFSET_X__ARRAY_of0$2);
  requires !(_WRITE_HAS_OCCURRED__ARRAY_if1234$1 && _WRITE_HAS_OCCURRED__ARRAY_if1234$2 && _WRITE_OFFSET_X__ARRAY_if1234$1 == _WRITE_OFFSET_X__ARRAY_if1234$2);
  requires !(_READ_HAS_OCCURRED__ARRAY_if1234$1 && _WRITE_HAS_OCCURRED__ARRAY_if1234$2 && _READ_OFFSET_X__ARRAY_if1234$1 == _WRITE_OFFSET_X__ARRAY_if1234$2);
  requires !(_WRITE_HAS_OCCURRED__ARRAY_of1234$1 && _WRITE_HAS_OCCURRED__ARRAY_of1234$2 && _WRITE_OFFSET_X__ARRAY_of1234$1 == _WRITE_OFFSET_X__ARRAY_of1234$2);
  requires !(_READ_HAS_OCCURRED__ARRAY_of1234$1 && _WRITE_HAS_OCCURRED__ARRAY_of1234$2 && _READ_OFFSET_X__ARRAY_of1234$1 == _WRITE_OFFSET_X__ARRAY_of1234$2);
  requires !(_WRITE_HAS_OCCURRED__ARRAY_if5678$1 && _WRITE_HAS_OCCURRED__ARRAY_if5678$2 && _WRITE_OFFSET_X__ARRAY_if5678$1 == _WRITE_OFFSET_X__ARRAY_if5678$2);
  requires !(_READ_HAS_OCCURRED__ARRAY_if5678$1 && _WRITE_HAS_OCCURRED__ARRAY_if5678$2 && _READ_OFFSET_X__ARRAY_if5678$1 == _WRITE_OFFSET_X__ARRAY_if5678$2);
  requires !(_WRITE_HAS_OCCURRED__ARRAY_of5678$1 && _WRITE_HAS_OCCURRED__ARRAY_of5678$2 && _WRITE_OFFSET_X__ARRAY_of5678$1 == _WRITE_OFFSET_X__ARRAY_of5678$2);
  requires !(_READ_HAS_OCCURRED__ARRAY_of5678$1 && _WRITE_HAS_OCCURRED__ARRAY_of5678$2 && _READ_OFFSET_X__ARRAY_of5678$1 == _WRITE_OFFSET_X__ARRAY_of5678$2);
  requires !(_WRITE_HAS_OCCURRED__ARRAY_typeVar$1 && _WRITE_HAS_OCCURRED__ARRAY_typeVar$2 && _WRITE_OFFSET_X__ARRAY_typeVar$1 == _WRITE_OFFSET_X__ARRAY_typeVar$2 && _ARRAY_typeVar$1[_WRITE_OFFSET_X__ARRAY_typeVar$1] != _ARRAY_typeVar$2[_WRITE_OFFSET_X__ARRAY_typeVar$2]);
  requires !(_READ_HAS_OCCURRED__ARRAY_typeVar$1 && _WRITE_HAS_OCCURRED__ARRAY_typeVar$2 && _READ_OFFSET_X__ARRAY_typeVar$1 == _WRITE_OFFSET_X__ARRAY_typeVar$2);
  requires !(_WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$1 && _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$2 && _WRITE_OFFSET_X__ARRAY_velocityBuffer$1 == _WRITE_OFFSET_X__ARRAY_velocityBuffer$2);
  requires !(_READ_HAS_OCCURRED__ARRAY_velocityBuffer$1 && _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$2 && _READ_OFFSET_X__ARRAY_velocityBuffer$1 == _WRITE_OFFSET_X__ARRAY_velocityBuffer$2);
  ensures !(_WRITE_HAS_OCCURRED__ARRAY_if0$1 && _WRITE_HAS_OCCURRED__ARRAY_if0$2 && _WRITE_OFFSET_X__ARRAY_if0$1 == _WRITE_OFFSET_X__ARRAY_if0$2);
  ensures !(_READ_HAS_OCCURRED__ARRAY_if0$1 && _WRITE_HAS_OCCURRED__ARRAY_if0$2 && _READ_OFFSET_X__ARRAY_if0$1 == _WRITE_OFFSET_X__ARRAY_if0$2);
  ensures !(_WRITE_HAS_OCCURRED__ARRAY_of0$1 && _WRITE_HAS_OCCURRED__ARRAY_of0$2 && _WRITE_OFFSET_X__ARRAY_of0$1 == _WRITE_OFFSET_X__ARRAY_of0$2);
  ensures !(_READ_HAS_OCCURRED__ARRAY_of0$1 && _WRITE_HAS_OCCURRED__ARRAY_of0$2 && _READ_OFFSET_X__ARRAY_of0$1 == _WRITE_OFFSET_X__ARRAY_of0$2);
  ensures !(_WRITE_HAS_OCCURRED__ARRAY_if1234$1 && _WRITE_HAS_OCCURRED__ARRAY_if1234$2 && _WRITE_OFFSET_X__ARRAY_if1234$1 == _WRITE_OFFSET_X__ARRAY_if1234$2);
  ensures !(_READ_HAS_OCCURRED__ARRAY_if1234$1 && _WRITE_HAS_OCCURRED__ARRAY_if1234$2 && _READ_OFFSET_X__ARRAY_if1234$1 == _WRITE_OFFSET_X__ARRAY_if1234$2);
  ensures !(_WRITE_HAS_OCCURRED__ARRAY_of1234$1 && _WRITE_HAS_OCCURRED__ARRAY_of1234$2 && _WRITE_OFFSET_X__ARRAY_of1234$1 == _WRITE_OFFSET_X__ARRAY_of1234$2);
  ensures !(_READ_HAS_OCCURRED__ARRAY_of1234$1 && _WRITE_HAS_OCCURRED__ARRAY_of1234$2 && _READ_OFFSET_X__ARRAY_of1234$1 == _WRITE_OFFSET_X__ARRAY_of1234$2);
  ensures !(_WRITE_HAS_OCCURRED__ARRAY_if5678$1 && _WRITE_HAS_OCCURRED__ARRAY_if5678$2 && _WRITE_OFFSET_X__ARRAY_if5678$1 == _WRITE_OFFSET_X__ARRAY_if5678$2);
  ensures !(_READ_HAS_OCCURRED__ARRAY_if5678$1 && _WRITE_HAS_OCCURRED__ARRAY_if5678$2 && _READ_OFFSET_X__ARRAY_if5678$1 == _WRITE_OFFSET_X__ARRAY_if5678$2);
  ensures !(_WRITE_HAS_OCCURRED__ARRAY_of5678$1 && _WRITE_HAS_OCCURRED__ARRAY_of5678$2 && _WRITE_OFFSET_X__ARRAY_of5678$1 == _WRITE_OFFSET_X__ARRAY_of5678$2);
  ensures !(_READ_HAS_OCCURRED__ARRAY_of5678$1 && _WRITE_HAS_OCCURRED__ARRAY_of5678$2 && _READ_OFFSET_X__ARRAY_of5678$1 == _WRITE_OFFSET_X__ARRAY_of5678$2);
  ensures !(_WRITE_HAS_OCCURRED__ARRAY_typeVar$1 && _WRITE_HAS_OCCURRED__ARRAY_typeVar$2 && _WRITE_OFFSET_X__ARRAY_typeVar$1 == _WRITE_OFFSET_X__ARRAY_typeVar$2 && _ARRAY_typeVar$1[_WRITE_OFFSET_X__ARRAY_typeVar$1] != _ARRAY_typeVar$2[_WRITE_OFFSET_X__ARRAY_typeVar$2]);
  ensures !(_READ_HAS_OCCURRED__ARRAY_typeVar$1 && _WRITE_HAS_OCCURRED__ARRAY_typeVar$2 && _READ_OFFSET_X__ARRAY_typeVar$1 == _WRITE_OFFSET_X__ARRAY_typeVar$2);
  ensures !(_WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$1 && _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$2 && _WRITE_OFFSET_X__ARRAY_velocityBuffer$1 == _WRITE_OFFSET_X__ARRAY_velocityBuffer$2);
  ensures !(_READ_HAS_OCCURRED__ARRAY_velocityBuffer$1 && _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$2 && _READ_OFFSET_X__ARRAY_velocityBuffer$1 == _WRITE_OFFSET_X__ARRAY_velocityBuffer$2);



implementation computefEq(_param_dir: double_2, _P$1: bool, _param_rho$1: double, _param_weight$1: double, _param_u$1: double_2, _P$2: bool, _param_rho$2: double, _param_weight$2: double, _param_u$2: double_2) returns (_returnVal$1: double, _returnVal$2: double)
{
  var rho$1: double;
  var rho$2: double;
  var weight$1: double;
  var weight$2: double;
  var dir$1: double_2;
  var dir$2: double_2;
  var u$1: double_2;
  var u$2: double_2;
  var eu$1: double;
  var eu$2: double;
  var u2$1: double;
  var u2$2: double;

  anon0:
    rho$1, rho$2 := (if _P$1 then _param_rho$1 else rho$1), (if _P$2 then _param_rho$2 else rho$2);
    weight$1, weight$2 := (if _P$1 then _param_weight$1 else weight$1), (if _P$2 then _param_weight$2 else weight$2);
    dir$1, dir$2 := (if _P$1 then _param_dir else dir$1), (if _P$2 then _param_dir else dir$2);
    u$1, u$2 := (if _P$1 then _param_u$1 else u$1), (if _P$2 then _param_u$2 else u$2);
    u2$1, u2$2 := (if _P$1 then DOUBLE_ADD(DOUBLE_MUL(double_2_extract_0(u$1), double_2_extract_0(u$1)), DOUBLE_MUL(double_2_extract_1(u$1), double_2_extract_1(u$1))) else u2$1), (if _P$2 then DOUBLE_ADD(DOUBLE_MUL(double_2_extract_0(u$2), double_2_extract_0(u$2)), DOUBLE_MUL(double_2_extract_1(u$2), double_2_extract_1(u$2))) else u2$2);
    eu$1, eu$2 := (if _P$1 then DOUBLE_ADD(DOUBLE_MUL(double_2_extract_0(dir$1), double_2_extract_0(u$1)), DOUBLE_MUL(double_2_extract_1(dir$1), double_2_extract_1(u$1))) else eu$1), (if _P$2 then DOUBLE_ADD(DOUBLE_MUL(double_2_extract_0(dir$2), double_2_extract_0(u$2)), DOUBLE_MUL(double_2_extract_1(dir$2), double_2_extract_1(u$2))) else eu$2);
    _returnVal$1, _returnVal$2 := (if _P$1 then DOUBLE_MUL(DOUBLE_MUL(rho$1, weight$1), DOUBLE_SUB(DOUBLE_ADD(DOUBLE_ADD(float_to_double(FLOAT_LITERAL(1065353216)), DOUBLE_MUL(float_to_double(FLOAT_LITERAL(1077936128)), eu$1)), DOUBLE_MUL(DOUBLE_MUL(float_to_double(FLOAT_LITERAL(1083179008)), eu$1), eu$1)), DOUBLE_MUL(float_to_double(FLOAT_LITERAL(1069547520)), u2$1))) else _returnVal$1), (if _P$2 then DOUBLE_MUL(DOUBLE_MUL(rho$2, weight$2), DOUBLE_SUB(DOUBLE_ADD(DOUBLE_ADD(float_to_double(FLOAT_LITERAL(1065353216)), DOUBLE_MUL(float_to_double(FLOAT_LITERAL(1077936128)), eu$2)), DOUBLE_MUL(DOUBLE_MUL(float_to_double(FLOAT_LITERAL(1083179008)), eu$2), eu$2)), DOUBLE_MUL(float_to_double(FLOAT_LITERAL(1069547520)), u2$2))) else _returnVal$2);
}



axiom bv32_to_bool(BV32_C_EQ(get_local_size.2, 1bv32));

axiom bv32_to_bool(BV32_C_EQ(get_num_groups.2, 1bv32));

axiom bv32_to_bool(BV32_C_EQ(get_num_groups.0, 1bv32));

axiom bv32_to_bool(BV32_C_EQ(get_num_groups.1, 256bv32));

axiom bv32_to_bool(BV32_C_EQ(get_local_size.0, 256bv32));

axiom bv32_to_bool(BV32_C_EQ(get_local_size.1, 1bv32));

function convert_int8_double_8_bv32_8(double_8) : bv32_8;

function dot_double_4_double_4_double(double_4, double_4) : double;

const unique _ARRAY_if0_BASE: _POINTER_BASE_global_double;

function __no_read__ARRAY_if0() : bool;

function __no_write__ARRAY_if0() : bool;

function __read__ARRAY_if0() : bool;

function __write__ARRAY_if0() : bool;

function __read_offset__ARRAY_if0() : bv32;

function __write_offset__ARRAY_if0() : bv32;

function __read_implies__ARRAY_if0(bool) : bool;

function __write_implies__ARRAY_if0(bool) : bool;

const unique _ARRAY_of0_BASE: _POINTER_BASE_global_double;

function __no_read__ARRAY_of0() : bool;

function __no_write__ARRAY_of0() : bool;

function __read__ARRAY_of0() : bool;

function __write__ARRAY_of0() : bool;

function __read_offset__ARRAY_of0() : bv32;

function __write_offset__ARRAY_of0() : bv32;

function __read_implies__ARRAY_of0(bool) : bool;

function __write_implies__ARRAY_of0(bool) : bool;

const unique _ARRAY_if1234_BASE: _POINTER_BASE_global_double_4;

function __no_read__ARRAY_if1234() : bool;

function __no_write__ARRAY_if1234() : bool;

function __read__ARRAY_if1234() : bool;

function __write__ARRAY_if1234() : bool;

function __read_offset__ARRAY_if1234() : bv32;

function __write_offset__ARRAY_if1234() : bv32;

function __read_implies__ARRAY_if1234(bool) : bool;

function __write_implies__ARRAY_if1234(bool) : bool;

const unique _ARRAY_of1234_BASE: _POINTER_BASE_global_double_4;

function __no_read__ARRAY_of1234() : bool;

function __no_write__ARRAY_of1234() : bool;

function __read__ARRAY_of1234() : bool;

function __write__ARRAY_of1234() : bool;

function __read_offset__ARRAY_of1234() : bv32;

function __write_offset__ARRAY_of1234() : bv32;

function __read_implies__ARRAY_of1234(bool) : bool;

function __write_implies__ARRAY_of1234(bool) : bool;

const unique _ARRAY_if5678_BASE: _POINTER_BASE_global_double_4;

function __no_read__ARRAY_if5678() : bool;

function __no_write__ARRAY_if5678() : bool;

function __read__ARRAY_if5678() : bool;

function __write__ARRAY_if5678() : bool;

function __read_offset__ARRAY_if5678() : bv32;

function __write_offset__ARRAY_if5678() : bv32;

function __read_implies__ARRAY_if5678(bool) : bool;

function __write_implies__ARRAY_if5678(bool) : bool;

const unique _ARRAY_of5678_BASE: _POINTER_BASE_global_double_4;

function __no_read__ARRAY_of5678() : bool;

function __no_write__ARRAY_of5678() : bool;

function __read__ARRAY_of5678() : bool;

function __write__ARRAY_of5678() : bool;

function __read_offset__ARRAY_of5678() : bv32;

function __write_offset__ARRAY_of5678() : bv32;

function __read_implies__ARRAY_of5678(bool) : bool;

function __write_implies__ARRAY_of5678(bool) : bool;

var {:global} _ARRAY_typeVar$1: [bv32]bool;

var {:global} _ARRAY_typeVar$2: [bv32]bool;

const unique _ARRAY_typeVar_BASE: _POINTER_BASE_global_bool;

function __no_read__ARRAY_typeVar() : bool;

function __no_write__ARRAY_typeVar() : bool;

function __read__ARRAY_typeVar() : bool;

function __write__ARRAY_typeVar() : bool;

function __read_offset__ARRAY_typeVar() : bv32;

function __write_offset__ARRAY_typeVar() : bv32;

function __read_implies__ARRAY_typeVar(bool) : bool;

function __write_implies__ARRAY_typeVar(bool) : bool;

var {:constant} _ARRAY_weight$1: [bv32]double;

var {:constant} _ARRAY_weight$2: [bv32]double;

const unique _ARRAY_weight_BASE: _POINTER_BASE_constant_double;

function __no_read__ARRAY_weight() : bool;

function __no_write__ARRAY_weight() : bool;

function __read__ARRAY_weight() : bool;

function __write__ARRAY_weight() : bool;

function __read_offset__ARRAY_weight() : bv32;

function __write_offset__ARRAY_weight() : bv32;

function __read_implies__ARRAY_weight(bool) : bool;

function __write_implies__ARRAY_weight(bool) : bool;

const unique _ARRAY_velocityBuffer_BASE: _POINTER_BASE_global_double_2;

function __no_read__ARRAY_velocityBuffer() : bool;

function __no_write__ARRAY_velocityBuffer() : bool;

function __read__ARRAY_velocityBuffer() : bool;

function __write__ARRAY_velocityBuffer() : bool;

function __read_offset__ARRAY_velocityBuffer() : bv32;

function __write_offset__ARRAY_velocityBuffer() : bv32;

function __read_implies__ARRAY_velocityBuffer(bool) : bool;

function __write_implies__ARRAY_velocityBuffer(bool) : bool;

type _POINTER_BASE_global_bool;

const unique _POINTER_BASE_global_bool_NULL: _POINTER_BASE_global_bool;

type {:datatype} _POINTER_TO_global_bool;

function {:constructor} _CONSTRUCT_POINTER_TO_global_bool(base: _POINTER_BASE_global_bool, offset: bv32) : _POINTER_TO_global_bool;

type _POINTER_BASE_global_double;

const unique _POINTER_BASE_global_double_NULL: _POINTER_BASE_global_double;

type {:datatype} _POINTER_TO_global_double;

function {:constructor} _CONSTRUCT_POINTER_TO_global_double(base: _POINTER_BASE_global_double, offset: bv32) : _POINTER_TO_global_double;

type _POINTER_BASE_constant_double;

const unique _POINTER_BASE_constant_double_NULL: _POINTER_BASE_constant_double;

type {:datatype} _POINTER_TO_constant_double;

function {:constructor} _CONSTRUCT_POINTER_TO_constant_double(base: _POINTER_BASE_constant_double, offset: bv32) : _POINTER_TO_constant_double;

type _POINTER_BASE_global_double_2;

const unique _POINTER_BASE_global_double_2_NULL: _POINTER_BASE_global_double_2;

type {:datatype} _POINTER_TO_global_double_2;

function {:constructor} _CONSTRUCT_POINTER_TO_global_double_2(base: _POINTER_BASE_global_double_2, offset: bv32) : _POINTER_TO_global_double_2;

type _POINTER_BASE_global_double_4;

const unique _POINTER_BASE_global_double_4_NULL: _POINTER_BASE_global_double_4;

type {:datatype} _POINTER_TO_global_double_4;

function {:constructor} _CONSTRUCT_POINTER_TO_global_double_4(base: _POINTER_BASE_global_double_4, offset: bv32) : _POINTER_TO_global_double_4;
















type float;

function FLOAT_LITERAL(int) : float;

function BV32_TO_FLOAT(bv32) : float;

function FLOAT_TO_BV32(float) : bv32;

function float_to_bv32(float) : bv32;

function float_to_double(float) : double;

function float_to_bv8(float) : bv8;

function bv8_to_float(bv8) : float;

function FLOAT_NEG(float) : float;

function FLOAT_ADD(float, float) : float;

function FLOAT_SUB(float, float) : float;

function FLOAT_MUL(float, float) : float;

function FLOAT_DIV(float, float) : float;

function {:inline true} FLOAT_MINUS(x: float) : float
{
  FLOAT_SUB(BV32_TO_FLOAT(0bv32), x)
}

function FLOAT_LT(float, float) : bool;

function FLOAT_LEQ(float, float) : bool;

function FLOAT_GT(float, float) : bool;

function FLOAT_GEQ(float, float) : bool;

function {:inline true} FLOAT_C_LT(x: float, y: float) : bv32
{
  (if FLOAT_LT(x, y) then 1bv32 else 0bv32)
}

function {:inline true} FLOAT_C_LEQ(x: float, y: float) : bv32
{
  (if FLOAT_LEQ(x, y) then 1bv32 else 0bv32)
}

function {:inline true} FLOAT_C_GT(x: float, y: float) : bv32
{
  (if FLOAT_GT(x, y) then 1bv32 else 0bv32)
}

function {:inline true} FLOAT_C_GEQ(x: float, y: float) : bv32
{
  (if FLOAT_GEQ(x, y) then 1bv32 else 0bv32)
}

function {:inline true} FLOAT_C_EQ(x: float, y: float) : bv32
{
  (if x == y then 1bv32 else 0bv32)
}

function {:inline true} FLOAT_C_NEQ(x: float, y: float) : bv32
{
  (if x != y then 1bv32 else 0bv32)
}

function bv32_to_float(bv32) : float;

type double;

function DOUBLE_LITERAL(int) : double;

function BV64_TO_DOUBLE(bv64) : double;

function DOUBLE_TO_BV64(double) : bv64;

function bv32_to_double(bv32) : double;

function double_to_bv8(double) : bv8;

function double_to_float(double) : float;

function DOUBLE_NEG(double) : double;

function DOUBLE_ADD(double, double) : double;

function DOUBLE_SUB(double, double) : double;

function DOUBLE_MUL(double, double) : double;

function DOUBLE_DIV(double, double) : double;

function {:inline 1} DOUBLE_MINUS(x: double) : double;

// autogenerated definition axiom
axiom (forall x: double :: {:inline 1} { DOUBLE_MINUS(x): double } DOUBLE_MINUS(x): double == DOUBLE_SUB(bv32_to_double(0bv32), x));

function DOUBLE_LT(double, double) : bool;

function DOUBLE_LEQ(double, double) : bool;

function DOUBLE_GT(double, double) : bool;

function DOUBLE_GEQ(double, double) : bool;

function {:inline true} DOUBLE_C_LT(x: double, y: double) : bv32
{
  (if DOUBLE_LT(x, y) then 1bv32 else 0bv32)
}

function {:inline true} DOUBLE_C_LEQ(x: double, y: double) : bv32
{
  (if DOUBLE_LEQ(x, y) then 1bv32 else 0bv32)
}

function {:inline true} DOUBLE_C_GT(x: double, y: double) : bv32
{
  (if DOUBLE_GT(x, y) then 1bv32 else 0bv32)
}

function {:inline true} DOUBLE_C_GEQ(x: double, y: double) : bv32
{
  (if DOUBLE_GEQ(x, y) then 1bv32 else 0bv32)
}

function {:inline true} DOUBLE_C_EQ(x: double, y: double) : bv32
{
  (if x == y then 1bv32 else 0bv32)
}

function bv64_to_double(bv64) : double;

function BV32_MUL_UNINTERPRETED(bv32, bv32) : bv32;

function BV32_DIV_UNINTERPRETED(bv32, bv32) : bv32;

function {:bvbuiltin "bvneg"} BV32_NEG(bv32) : bv32;

function {:bvbuiltin "bvadd"} BV32_ADD(bv32, bv32) : bv32;

function {:bvbuiltin "bvsub"} BV32_SUB(bv32, bv32) : bv32;

function {:bvbuiltin "bvmul"} BV32_MUL(bv32, bv32) : bv32;

function {:bvbuiltin "bvudiv"} BV32_DIV(bv32, bv32) : bv32;

function {:bvbuiltin "bvshl"} BV32_SHL(bv32, bv32) : bv32;

function {:bvbuiltin "bvsrem_i"} BV32_SREM(bv32, bv32) : bv32;

function {:bvbuiltin "bvurem_i"} BV32_UREM(bv32, bv32) : bv32;

function {:inline true} BV32_MINUS(x: bv32) : bv32
{
  BV32_SUB(0bv32, x)
}

function {:bvbuiltin "bvashr"} BV32_ASHR(bv32, bv32) : bv32;

function {:bvbuiltin "bvlshr"} BV32_LSHR(bv32, bv32) : bv32;

function {:bvbuiltin "bvumul_noovfl"} BV32_UMUL_NOOVFL(bv32, bv32) : bv32;

function {:bvbuiltin "bvsmul_noovfl"} BV32_SMUL_NOOVFL(bv32, bv32) : bv32;

function {:bvbuiltin "bvsmul_noudfl"} BV32_SMUL_NOUDFL(bv32, bv32) : bv32;

function {:bvbuiltin "bvmul"} BV32_MUL24(bv32, bv32) : bv32;

function {:bvbuiltin "bvult"} BV32_ULT(bv32, bv32) : bool;

function {:bvbuiltin "bvslt"} BV32_LT(bv32, bv32) : bool;

function {:bvbuiltin "bvule"} BV32_ULEQ(bv32, bv32) : bool;

function {:bvbuiltin "bvsle"} BV32_LEQ(bv32, bv32) : bool;

function {:bvbuiltin "bvugt"} BV32_UGT(bv32, bv32) : bool;

function {:bvbuiltin "bvsgt"} BV32_GT(bv32, bv32) : bool;

function {:bvbuiltin "bvuge"} BV32_UGEQ(bv32, bv32) : bool;

function {:bvbuiltin "bvsge"} BV32_GEQ(bv32, bv32) : bool;

function {:bvbuiltin "bvand"} BV32_AND(bv32, bv32) : bv32;

function {:bvbuiltin "bvor"} BV32_OR(bv32, bv32) : bv32;

function {:bvbuiltin "bvxor"} BV32_XOR(bv32, bv32) : bv32;

function {:bvbuiltin "bvnot"} BV32_NOT(bv32) : bv32;

function {:inline true} BV32_EQ(x: bv32, y: bv32) : bool
{
  x == y
}

function {:inline true} BV32_NEQ(x: bv32, y: bv32) : bool
{
  x != y
}

function {:inline true} BV32_C_ULT(x: bv32, y: bv32) : bv32
{
  (if BV32_ULT(x, y) then 1bv32 else 0bv32)
}

function {:inline true} BV32_C_LT(x: bv32, y: bv32) : bv32
{
  (if BV32_LT(x, y) then 1bv32 else 0bv32)
}

function {:inline true} BV32_C_ULEQ(x: bv32, y: bv32) : bv32
{
  (if BV32_ULEQ(x, y) then 1bv32 else 0bv32)
}

function {:inline true} BV32_C_LEQ(x: bv32, y: bv32) : bv32
{
  (if BV32_LEQ(x, y) then 1bv32 else 0bv32)
}

function {:inline true} BV32_C_UGT(x: bv32, y: bv32) : bv32
{
  (if BV32_UGT(x, y) then 1bv32 else 0bv32)
}

function {:inline true} BV32_C_GT(x: bv32, y: bv32) : bv32
{
  (if BV32_GT(x, y) then 1bv32 else 0bv32)
}

function {:inline true} BV32_C_UGEQ(x: bv32, y: bv32) : bv32
{
  (if BV32_UGEQ(x, y) then 1bv32 else 0bv32)
}

function {:inline true} BV32_C_GEQ(x: bv32, y: bv32) : bv32
{
  (if BV32_GEQ(x, y) then 1bv32 else 0bv32)
}

function {:inline true} BV32_C_EQ(x: bv32, y: bv32) : bv32
{
  (if x == y then 1bv32 else 0bv32)
}

function {:inline true} BV32_C_NEQ(x: bv32, y: bv32) : bv32
{
  (if x != y then 1bv32 else 0bv32)
}

function {:inline true} BV32_C_LAND(x: bv32, y: bv32) : bv32
{
  (if bv32_to_bool(x) && bv32_to_bool(y) then 1bv32 else 0bv32)
}

function {:inline true} BV32_C_LOR(x: bv32, y: bv32) : bv32
{
  (if bv32_to_bool(x) || bv32_to_bool(y) then 1bv32 else 0bv32)
}

function {:inline true} BV32_C_LNOT(x: bv32) : bv32
{
  (if x == 0bv32 then 0bv32 else 1bv32)
}

function {:inline true} BOOL_C_LNOT(x: bool) : bv32
{
  (if !x then 0bv32 else 1bv32)
}

function {:inline true} BOOL_LAND(x: bool, y: bool) : bool
{
  x && y
}

function {:inline true} BOOL_LOR(x: bool, y: bool) : bool
{
  x || y
}

function {:inline true} bv32_to_bool(x: bv32) : bool
{
  x != 0bv32
}

function {:inline true} bool_to_bv32(x: bool) : bv32
{
  (if x then 1bv32 else 0bv32)
}

type {:datatype} float_2;

type {:datatype} float_3;

type {:datatype} float_4;

type {:datatype} float_8;

type {:datatype} float_16;

function {:constructor} construct_float_2.1_1(x: float, y: float) : float_2;

function {:constructor} construct_float_3.1_1_1(x: float, y: float, z: float) : float_3;

function {:constructor} construct_float_4.1_1_1_1(x: float, y: float, z: float, w: float) : float_4;

function {:constructor} construct_float_8.1_1_1_1_1_1_1_1(s0: float, s1: float, s2: float, s3: float, s4: float, s5: float, s6: float, s7: float) : float_8;

function {:constructor} construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0: float, s1: float, s2: float, s3: float, s4: float, s5: float, s6: float, s7: float, s8: float, s9: float, sa: float, sb: float, sc: float, sd: float, se: float, sf: float) : float_16;

function {:inline true} construct_float_3.1_2(x: float, yz: float_2) : float_3
{
  construct_float_3.1_1_1(x, x#construct_float_2.1_1(yz), y#construct_float_2.1_1(yz))
}

function {:inline true} construct_float_3.2_1(xy: float_2, z: float) : float_3
{
  construct_float_3.1_1_1(x#construct_float_2.1_1(xy), y#construct_float_2.1_1(xy), z)
}

function {:inline true} construct_float_4.1_1_2(x: float, y: float, zw: float_2) : float_4
{
  construct_float_4.1_1_1_1(x, y, x#construct_float_2.1_1(zw), y#construct_float_2.1_1(zw))
}

function {:inline true} construct_float_4.1_2_1(x: float, yz: float_2, w: float) : float_4
{
  construct_float_4.1_1_1_1(x, x#construct_float_2.1_1(yz), y#construct_float_2.1_1(yz), w)
}

function {:inline true} construct_float_4.1_3(x: float, yzw: float_3) : float_4
{
  construct_float_4.1_1_1_1(x, x#construct_float_3.1_1_1(yzw), y#construct_float_3.1_1_1(yzw), z#construct_float_3.1_1_1(yzw))
}

function {:inline true} construct_float_4.2_1_1(xy: float_2, z: float, w: float) : float_4
{
  construct_float_4.1_1_1_1(x#construct_float_2.1_1(xy), y#construct_float_2.1_1(xy), z, w)
}

function {:inline true} construct_float_4.2_2(xy: float_2, zw: float_2) : float_4
{
  construct_float_4.1_1_1_1(x#construct_float_2.1_1(xy), y#construct_float_2.1_1(xy), x#construct_float_2.1_1(zw), y#construct_float_2.1_1(zw))
}

function {:inline true} construct_float_4.3_1(xyz: float_3, w: float) : float_4
{
  construct_float_4.1_1_1_1(x#construct_float_3.1_1_1(xyz), y#construct_float_3.1_1_1(xyz), z#construct_float_3.1_1_1(xyz), w)
}

function {:inline true} construct_float_8.4_4(s0s1s2s3: float_4, s4s5s6s7: float_4) : float_8
{
  construct_float_8.1_1_1_1_1_1_1_1(x#construct_float_4.1_1_1_1(s0s1s2s3), y#construct_float_4.1_1_1_1(s0s1s2s3), z#construct_float_4.1_1_1_1(s0s1s2s3), w#construct_float_4.1_1_1_1(s0s1s2s3), x#construct_float_4.1_1_1_1(s4s5s6s7), y#construct_float_4.1_1_1_1(s4s5s6s7), z#construct_float_4.1_1_1_1(s4s5s6s7), w#construct_float_4.1_1_1_1(s4s5s6s7))
}

function {:inline true} float_2_insert_0(v: float_2, x: float) : float_2
{
  construct_float_2.1_1(x, y#construct_float_2.1_1(v))
}

function {:inline true} float_2_insert_1(v: float_2, y: float) : float_2
{
  construct_float_2.1_1(x#construct_float_2.1_1(v), y)
}

function {:inline true} float_3_insert_0(v: float_3, x: float) : float_3
{
  construct_float_3.1_1_1(x, y#construct_float_3.1_1_1(v), z#construct_float_3.1_1_1(v))
}

function {:inline true} float_3_insert_1(v: float_3, y: float) : float_3
{
  construct_float_3.1_1_1(x#construct_float_3.1_1_1(v), y, z#construct_float_3.1_1_1(v))
}

function {:inline true} float_3_insert_2(v: float_3, z: float) : float_3
{
  construct_float_3.1_1_1(x#construct_float_3.1_1_1(v), y#construct_float_3.1_1_1(v), z)
}

function {:inline true} float_4_insert_0(v: float_4, x: float) : float_4
{
  construct_float_4.1_1_1_1(x, y#construct_float_4.1_1_1_1(v), z#construct_float_4.1_1_1_1(v), w#construct_float_4.1_1_1_1(v))
}

function {:inline true} float_4_insert_1(v: float_4, y: float) : float_4
{
  construct_float_4.1_1_1_1(x#construct_float_4.1_1_1_1(v), y, z#construct_float_4.1_1_1_1(v), w#construct_float_4.1_1_1_1(v))
}

function {:inline true} float_4_insert_2(v: float_4, z: float) : float_4
{
  construct_float_4.1_1_1_1(x#construct_float_4.1_1_1_1(v), y#construct_float_4.1_1_1_1(v), z, w#construct_float_4.1_1_1_1(v))
}

function {:inline true} float_4_insert_3(v: float_4, w: float) : float_4
{
  construct_float_4.1_1_1_1(x#construct_float_4.1_1_1_1(v), y#construct_float_4.1_1_1_1(v), z#construct_float_4.1_1_1_1(v), w)
}

function {:inline true} float_8_insert_0(v: float_8, s0: float) : float_8
{
  construct_float_8.1_1_1_1_1_1_1_1(s0, s1#construct_float_8.1_1_1_1_1_1_1_1(v), s2#construct_float_8.1_1_1_1_1_1_1_1(v), s3#construct_float_8.1_1_1_1_1_1_1_1(v), s4#construct_float_8.1_1_1_1_1_1_1_1(v), s5#construct_float_8.1_1_1_1_1_1_1_1(v), s6#construct_float_8.1_1_1_1_1_1_1_1(v), s7#construct_float_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_8_insert_1(v: float_8, s1: float) : float_8
{
  construct_float_8.1_1_1_1_1_1_1_1(s0#construct_float_8.1_1_1_1_1_1_1_1(v), s1, s2#construct_float_8.1_1_1_1_1_1_1_1(v), s3#construct_float_8.1_1_1_1_1_1_1_1(v), s4#construct_float_8.1_1_1_1_1_1_1_1(v), s5#construct_float_8.1_1_1_1_1_1_1_1(v), s6#construct_float_8.1_1_1_1_1_1_1_1(v), s7#construct_float_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_8_insert_2(v: float_8, s2: float) : float_8
{
  construct_float_8.1_1_1_1_1_1_1_1(s0#construct_float_8.1_1_1_1_1_1_1_1(v), s1#construct_float_8.1_1_1_1_1_1_1_1(v), s2, s3#construct_float_8.1_1_1_1_1_1_1_1(v), s4#construct_float_8.1_1_1_1_1_1_1_1(v), s5#construct_float_8.1_1_1_1_1_1_1_1(v), s6#construct_float_8.1_1_1_1_1_1_1_1(v), s7#construct_float_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_8_insert_3(v: float_8, s3: float) : float_8
{
  construct_float_8.1_1_1_1_1_1_1_1(s0#construct_float_8.1_1_1_1_1_1_1_1(v), s1#construct_float_8.1_1_1_1_1_1_1_1(v), s2#construct_float_8.1_1_1_1_1_1_1_1(v), s3, s4#construct_float_8.1_1_1_1_1_1_1_1(v), s5#construct_float_8.1_1_1_1_1_1_1_1(v), s6#construct_float_8.1_1_1_1_1_1_1_1(v), s7#construct_float_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_8_insert_4(v: float_8, s4: float) : float_8
{
  construct_float_8.1_1_1_1_1_1_1_1(s0#construct_float_8.1_1_1_1_1_1_1_1(v), s1#construct_float_8.1_1_1_1_1_1_1_1(v), s2#construct_float_8.1_1_1_1_1_1_1_1(v), s3#construct_float_8.1_1_1_1_1_1_1_1(v), s4, s5#construct_float_8.1_1_1_1_1_1_1_1(v), s6#construct_float_8.1_1_1_1_1_1_1_1(v), s7#construct_float_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_8_insert_5(v: float_8, s5: float) : float_8
{
  construct_float_8.1_1_1_1_1_1_1_1(s0#construct_float_8.1_1_1_1_1_1_1_1(v), s1#construct_float_8.1_1_1_1_1_1_1_1(v), s2#construct_float_8.1_1_1_1_1_1_1_1(v), s3#construct_float_8.1_1_1_1_1_1_1_1(v), s4#construct_float_8.1_1_1_1_1_1_1_1(v), s5, s6#construct_float_8.1_1_1_1_1_1_1_1(v), s7#construct_float_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_8_insert_6(v: float_8, s6: float) : float_8
{
  construct_float_8.1_1_1_1_1_1_1_1(s0#construct_float_8.1_1_1_1_1_1_1_1(v), s1#construct_float_8.1_1_1_1_1_1_1_1(v), s2#construct_float_8.1_1_1_1_1_1_1_1(v), s3#construct_float_8.1_1_1_1_1_1_1_1(v), s4#construct_float_8.1_1_1_1_1_1_1_1(v), s5#construct_float_8.1_1_1_1_1_1_1_1(v), s6, s7#construct_float_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_8_insert_7(v: float_8, s7: float) : float_8
{
  construct_float_8.1_1_1_1_1_1_1_1(s0#construct_float_8.1_1_1_1_1_1_1_1(v), s1#construct_float_8.1_1_1_1_1_1_1_1(v), s2#construct_float_8.1_1_1_1_1_1_1_1(v), s3#construct_float_8.1_1_1_1_1_1_1_1(v), s4#construct_float_8.1_1_1_1_1_1_1_1(v), s5#construct_float_8.1_1_1_1_1_1_1_1(v), s6#construct_float_8.1_1_1_1_1_1_1_1(v), s7)
}

function {:inline true} float_16_insert_0(v: float_16, s0: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0, s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_1(v: float_16, s1: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1, s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_2(v: float_16, s2: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2, s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_3(v: float_16, s3: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3, s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_4(v: float_16, s4: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4, s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_5(v: float_16, s5: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5, s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_6(v: float_16, s6: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6, s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_7(v: float_16, s7: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7, s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_8(v: float_16, s8: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8, s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_9(v: float_16, s9: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9, sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_10(v: float_16, sa: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa, sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_11(v: float_16, sb: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb, sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_12(v: float_16, sc: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc, sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_13(v: float_16, sd: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd, se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_14(v: float_16, se: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se, sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} float_16_insert_15(v: float_16, sf: float) : float_16
{
  construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf)
}

function {:inline true} float_2_extract_0(v: float_2) : float
{
  x#construct_float_2.1_1(v)
}

function {:inline true} float_2_extract_1(v: float_2) : float
{
  y#construct_float_2.1_1(v)
}

function {:inline true} float_3_extract_0(v: float_3) : float
{
  x#construct_float_3.1_1_1(v)
}

function {:inline true} float_3_extract_1(v: float_3) : float
{
  y#construct_float_3.1_1_1(v)
}

function {:inline true} float_3_extract_2(v: float_3) : float
{
  z#construct_float_3.1_1_1(v)
}

function {:inline true} float_4_extract_0(v: float_4) : float
{
  x#construct_float_4.1_1_1_1(v)
}

function {:inline true} float_4_extract_1(v: float_4) : float
{
  y#construct_float_4.1_1_1_1(v)
}

function {:inline true} float_4_extract_2(v: float_4) : float
{
  z#construct_float_4.1_1_1_1(v)
}

function {:inline true} float_4_extract_3(v: float_4) : float
{
  w#construct_float_4.1_1_1_1(v)
}

function {:inline true} float_8_extract_0(v: float_8) : float
{
  s0#construct_float_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_8_extract_1(v: float_8) : float
{
  s1#construct_float_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_8_extract_2(v: float_8) : float
{
  s2#construct_float_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_8_extract_3(v: float_8) : float
{
  s3#construct_float_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_8_extract_4(v: float_8) : float
{
  s4#construct_float_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_8_extract_5(v: float_8) : float
{
  s5#construct_float_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_8_extract_6(v: float_8) : float
{
  s6#construct_float_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_8_extract_7(v: float_8) : float
{
  s7#construct_float_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_0(v: float_16) : float
{
  s0#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_1(v: float_16) : float
{
  s1#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_2(v: float_16) : float
{
  s2#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_3(v: float_16) : float
{
  s3#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_4(v: float_16) : float
{
  s4#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_5(v: float_16) : float
{
  s5#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_6(v: float_16) : float
{
  s6#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_7(v: float_16) : float
{
  s7#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_8(v: float_16) : float
{
  s8#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_9(v: float_16) : float
{
  s9#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_10(v: float_16) : float
{
  sa#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_11(v: float_16) : float
{
  sb#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_12(v: float_16) : float
{
  sc#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_13(v: float_16) : float
{
  sd#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_14(v: float_16) : float
{
  se#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} float_16_extract_15(v: float_16) : float
{
  sf#construct_float_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}







































type {:datatype} bv32_2;

type {:datatype} bv32_3;

type {:datatype} bv32_4;

type {:datatype} bv32_8;

type {:datatype} bv32_16;

function {:constructor} construct_bv32_2.1_1(x: bv32, y: bv32) : bv32_2;

function {:constructor} construct_bv32_3.1_1_1(x: bv32, y: bv32, z: bv32) : bv32_3;

function {:constructor} construct_bv32_4.1_1_1_1(x: bv32, y: bv32, z: bv32, w: bv32) : bv32_4;

function {:constructor} construct_bv32_8.1_1_1_1_1_1_1_1(s0: bv32, s1: bv32, s2: bv32, s3: bv32, s4: bv32, s5: bv32, s6: bv32, s7: bv32) : bv32_8;

function {:constructor} construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0: bv32, s1: bv32, s2: bv32, s3: bv32, s4: bv32, s5: bv32, s6: bv32, s7: bv32, s8: bv32, s9: bv32, sa: bv32, sb: bv32, sc: bv32, sd: bv32, se: bv32, sf: bv32) : bv32_16;

function {:inline true} construct_bv32_3.1_2(x: bv32, yz: bv32_2) : bv32_3
{
  construct_bv32_3.1_1_1(x, x#construct_bv32_2.1_1(yz), y#construct_bv32_2.1_1(yz))
}

function {:inline true} construct_bv32_3.2_1(xy: bv32_2, z: bv32) : bv32_3
{
  construct_bv32_3.1_1_1(x#construct_bv32_2.1_1(xy), y#construct_bv32_2.1_1(xy), z)
}

function {:inline true} construct_bv32_4.1_1_2(x: bv32, y: bv32, zw: bv32_2) : bv32_4
{
  construct_bv32_4.1_1_1_1(x, y, x#construct_bv32_2.1_1(zw), y#construct_bv32_2.1_1(zw))
}

function {:inline true} construct_bv32_4.1_2_1(x: bv32, yz: bv32_2, w: bv32) : bv32_4
{
  construct_bv32_4.1_1_1_1(x, x#construct_bv32_2.1_1(yz), y#construct_bv32_2.1_1(yz), w)
}

function {:inline true} construct_bv32_4.1_3(x: bv32, yzw: bv32_3) : bv32_4
{
  construct_bv32_4.1_1_1_1(x, x#construct_bv32_3.1_1_1(yzw), y#construct_bv32_3.1_1_1(yzw), z#construct_bv32_3.1_1_1(yzw))
}

function {:inline true} construct_bv32_4.2_1_1(xy: bv32_2, z: bv32, w: bv32) : bv32_4
{
  construct_bv32_4.1_1_1_1(x#construct_bv32_2.1_1(xy), y#construct_bv32_2.1_1(xy), z, w)
}

function {:inline true} construct_bv32_4.2_2(xy: bv32_2, zw: bv32_2) : bv32_4
{
  construct_bv32_4.1_1_1_1(x#construct_bv32_2.1_1(xy), y#construct_bv32_2.1_1(xy), x#construct_bv32_2.1_1(zw), y#construct_bv32_2.1_1(zw))
}

function {:inline true} construct_bv32_4.3_1(xyz: bv32_3, w: bv32) : bv32_4
{
  construct_bv32_4.1_1_1_1(x#construct_bv32_3.1_1_1(xyz), y#construct_bv32_3.1_1_1(xyz), z#construct_bv32_3.1_1_1(xyz), w)
}

function {:inline true} bv32_2_insert_0(v: bv32_2, x: bv32) : bv32_2
{
  construct_bv32_2.1_1(x, y#construct_bv32_2.1_1(v))
}

function {:inline true} bv32_2_insert_1(v: bv32_2, y: bv32) : bv32_2
{
  construct_bv32_2.1_1(x#construct_bv32_2.1_1(v), y)
}

function {:inline true} bv32_3_insert_0(v: bv32_3, x: bv32) : bv32_3
{
  construct_bv32_3.1_1_1(x, y#construct_bv32_3.1_1_1(v), z#construct_bv32_3.1_1_1(v))
}

function {:inline true} bv32_3_insert_1(v: bv32_3, y: bv32) : bv32_3
{
  construct_bv32_3.1_1_1(x#construct_bv32_3.1_1_1(v), y, z#construct_bv32_3.1_1_1(v))
}

function {:inline true} bv32_3_insert_2(v: bv32_3, z: bv32) : bv32_3
{
  construct_bv32_3.1_1_1(x#construct_bv32_3.1_1_1(v), y#construct_bv32_3.1_1_1(v), z)
}

function {:inline true} bv32_4_insert_0(v: bv32_4, x: bv32) : bv32_4
{
  construct_bv32_4.1_1_1_1(x, y#construct_bv32_4.1_1_1_1(v), z#construct_bv32_4.1_1_1_1(v), w#construct_bv32_4.1_1_1_1(v))
}

function {:inline true} bv32_4_insert_1(v: bv32_4, y: bv32) : bv32_4
{
  construct_bv32_4.1_1_1_1(x#construct_bv32_4.1_1_1_1(v), y, z#construct_bv32_4.1_1_1_1(v), w#construct_bv32_4.1_1_1_1(v))
}

function {:inline true} bv32_4_insert_2(v: bv32_4, z: bv32) : bv32_4
{
  construct_bv32_4.1_1_1_1(x#construct_bv32_4.1_1_1_1(v), y#construct_bv32_4.1_1_1_1(v), z, w#construct_bv32_4.1_1_1_1(v))
}

function {:inline true} bv32_4_insert_3(v: bv32_4, w: bv32) : bv32_4
{
  construct_bv32_4.1_1_1_1(x#construct_bv32_4.1_1_1_1(v), y#construct_bv32_4.1_1_1_1(v), z#construct_bv32_4.1_1_1_1(v), w)
}

function {:inline true} bv32_8_insert_0(v: bv32_8, s0: bv32) : bv32_8
{
  construct_bv32_8.1_1_1_1_1_1_1_1(s0, s1#construct_bv32_8.1_1_1_1_1_1_1_1(v), s2#construct_bv32_8.1_1_1_1_1_1_1_1(v), s3#construct_bv32_8.1_1_1_1_1_1_1_1(v), s4#construct_bv32_8.1_1_1_1_1_1_1_1(v), s5#construct_bv32_8.1_1_1_1_1_1_1_1(v), s6#construct_bv32_8.1_1_1_1_1_1_1_1(v), s7#construct_bv32_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_8_insert_1(v: bv32_8, s1: bv32) : bv32_8
{
  construct_bv32_8.1_1_1_1_1_1_1_1(s0#construct_bv32_8.1_1_1_1_1_1_1_1(v), s1, s2#construct_bv32_8.1_1_1_1_1_1_1_1(v), s3#construct_bv32_8.1_1_1_1_1_1_1_1(v), s4#construct_bv32_8.1_1_1_1_1_1_1_1(v), s5#construct_bv32_8.1_1_1_1_1_1_1_1(v), s6#construct_bv32_8.1_1_1_1_1_1_1_1(v), s7#construct_bv32_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_8_insert_2(v: bv32_8, s2: bv32) : bv32_8
{
  construct_bv32_8.1_1_1_1_1_1_1_1(s0#construct_bv32_8.1_1_1_1_1_1_1_1(v), s1#construct_bv32_8.1_1_1_1_1_1_1_1(v), s2, s3#construct_bv32_8.1_1_1_1_1_1_1_1(v), s4#construct_bv32_8.1_1_1_1_1_1_1_1(v), s5#construct_bv32_8.1_1_1_1_1_1_1_1(v), s6#construct_bv32_8.1_1_1_1_1_1_1_1(v), s7#construct_bv32_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_8_insert_3(v: bv32_8, s3: bv32) : bv32_8
{
  construct_bv32_8.1_1_1_1_1_1_1_1(s0#construct_bv32_8.1_1_1_1_1_1_1_1(v), s1#construct_bv32_8.1_1_1_1_1_1_1_1(v), s2#construct_bv32_8.1_1_1_1_1_1_1_1(v), s3, s4#construct_bv32_8.1_1_1_1_1_1_1_1(v), s5#construct_bv32_8.1_1_1_1_1_1_1_1(v), s6#construct_bv32_8.1_1_1_1_1_1_1_1(v), s7#construct_bv32_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_8_insert_4(v: bv32_8, s4: bv32) : bv32_8
{
  construct_bv32_8.1_1_1_1_1_1_1_1(s0#construct_bv32_8.1_1_1_1_1_1_1_1(v), s1#construct_bv32_8.1_1_1_1_1_1_1_1(v), s2#construct_bv32_8.1_1_1_1_1_1_1_1(v), s3#construct_bv32_8.1_1_1_1_1_1_1_1(v), s4, s5#construct_bv32_8.1_1_1_1_1_1_1_1(v), s6#construct_bv32_8.1_1_1_1_1_1_1_1(v), s7#construct_bv32_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_8_insert_5(v: bv32_8, s5: bv32) : bv32_8
{
  construct_bv32_8.1_1_1_1_1_1_1_1(s0#construct_bv32_8.1_1_1_1_1_1_1_1(v), s1#construct_bv32_8.1_1_1_1_1_1_1_1(v), s2#construct_bv32_8.1_1_1_1_1_1_1_1(v), s3#construct_bv32_8.1_1_1_1_1_1_1_1(v), s4#construct_bv32_8.1_1_1_1_1_1_1_1(v), s5, s6#construct_bv32_8.1_1_1_1_1_1_1_1(v), s7#construct_bv32_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_8_insert_6(v: bv32_8, s6: bv32) : bv32_8
{
  construct_bv32_8.1_1_1_1_1_1_1_1(s0#construct_bv32_8.1_1_1_1_1_1_1_1(v), s1#construct_bv32_8.1_1_1_1_1_1_1_1(v), s2#construct_bv32_8.1_1_1_1_1_1_1_1(v), s3#construct_bv32_8.1_1_1_1_1_1_1_1(v), s4#construct_bv32_8.1_1_1_1_1_1_1_1(v), s5#construct_bv32_8.1_1_1_1_1_1_1_1(v), s6, s7#construct_bv32_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_8_insert_7(v: bv32_8, s7: bv32) : bv32_8
{
  construct_bv32_8.1_1_1_1_1_1_1_1(s0#construct_bv32_8.1_1_1_1_1_1_1_1(v), s1#construct_bv32_8.1_1_1_1_1_1_1_1(v), s2#construct_bv32_8.1_1_1_1_1_1_1_1(v), s3#construct_bv32_8.1_1_1_1_1_1_1_1(v), s4#construct_bv32_8.1_1_1_1_1_1_1_1(v), s5#construct_bv32_8.1_1_1_1_1_1_1_1(v), s6#construct_bv32_8.1_1_1_1_1_1_1_1(v), s7)
}

function {:inline true} bv32_16_insert_0(v: bv32_16, s0: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0, s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_1(v: bv32_16, s1: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1, s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_2(v: bv32_16, s2: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2, s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_3(v: bv32_16, s3: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3, s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_4(v: bv32_16, s4: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4, s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_5(v: bv32_16, s5: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5, s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_6(v: bv32_16, s6: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6, s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_7(v: bv32_16, s7: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7, s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_8(v: bv32_16, s8: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8, s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_9(v: bv32_16, s9: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9, sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_10(v: bv32_16, sa: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa, sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_11(v: bv32_16, sb: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb, sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_12(v: bv32_16, sc: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc, sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_13(v: bv32_16, sd: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd, se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_14(v: bv32_16, se: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se, sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v))
}

function {:inline true} bv32_16_insert_15(v: bv32_16, sf: bv32) : bv32_16
{
  construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v), sf)
}

function {:inline true} bv32_2_extract_0(v: bv32_2) : bv32
{
  x#construct_bv32_2.1_1(v)
}

function {:inline true} bv32_2_extract_1(v: bv32_2) : bv32
{
  y#construct_bv32_2.1_1(v)
}

function {:inline true} bv32_3_extract_0(v: bv32_3) : bv32
{
  x#construct_bv32_3.1_1_1(v)
}

function {:inline true} bv32_3_extract_1(v: bv32_3) : bv32
{
  y#construct_bv32_3.1_1_1(v)
}

function {:inline true} bv32_3_extract_2(v: bv32_3) : bv32
{
  z#construct_bv32_3.1_1_1(v)
}

function {:inline true} bv32_4_extract_0(v: bv32_4) : bv32
{
  x#construct_bv32_4.1_1_1_1(v)
}

function {:inline true} bv32_4_extract_1(v: bv32_4) : bv32
{
  y#construct_bv32_4.1_1_1_1(v)
}

function {:inline true} bv32_4_extract_2(v: bv32_4) : bv32
{
  z#construct_bv32_4.1_1_1_1(v)
}

function {:inline true} bv32_4_extract_3(v: bv32_4) : bv32
{
  w#construct_bv32_4.1_1_1_1(v)
}

function {:inline true} bv32_8_extract_0(v: bv32_8) : bv32
{
  s0#construct_bv32_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_8_extract_1(v: bv32_8) : bv32
{
  s1#construct_bv32_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_8_extract_2(v: bv32_8) : bv32
{
  s2#construct_bv32_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_8_extract_3(v: bv32_8) : bv32
{
  s3#construct_bv32_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_8_extract_4(v: bv32_8) : bv32
{
  s4#construct_bv32_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_8_extract_5(v: bv32_8) : bv32
{
  s5#construct_bv32_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_8_extract_6(v: bv32_8) : bv32
{
  s6#construct_bv32_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_8_extract_7(v: bv32_8) : bv32
{
  s7#construct_bv32_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_0(v: bv32_16) : bv32
{
  s0#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_1(v: bv32_16) : bv32
{
  s1#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_2(v: bv32_16) : bv32
{
  s2#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_3(v: bv32_16) : bv32
{
  s3#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_4(v: bv32_16) : bv32
{
  s4#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_5(v: bv32_16) : bv32
{
  s5#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_6(v: bv32_16) : bv32
{
  s6#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_7(v: bv32_16) : bv32
{
  s7#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_8(v: bv32_16) : bv32
{
  s8#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_9(v: bv32_16) : bv32
{
  s9#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_10(v: bv32_16) : bv32
{
  sa#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_11(v: bv32_16) : bv32
{
  sb#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_12(v: bv32_16) : bv32
{
  sc#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_13(v: bv32_16) : bv32
{
  sd#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_14(v: bv32_16) : bv32
{
  se#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}

function {:inline true} bv32_16_extract_15(v: bv32_16) : bv32
{
  sf#construct_bv32_16.1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1(v)
}







































type {:datatype} double_2;

type {:datatype} double_3;

type {:datatype} double_4;

type {:datatype} double_8;

function {:constructor} construct_double_2.1_1(x: double, y: double) : double_2;

function {:constructor} construct_double_3.1_1_1(x: double, y: double, z: double) : double_3;

function {:constructor} construct_double_4.1_1_1_1(x: double, y: double, z: double, w: double) : double_4;

function {:constructor} construct_double_8.1_1_1_1_1_1_1_1(s0: double, s1: double, s2: double, s3: double, s4: double, s5: double, s6: double, s7: double) : double_8;

function {:inline true} construct_double_3.1_2(x: double, yz: double_2) : double_3
{
  construct_double_3.1_1_1(x, x#construct_double_2.1_1(yz), y#construct_double_2.1_1(yz))
}

function {:inline true} construct_double_3.2_1(xy: double_2, z: double) : double_3
{
  construct_double_3.1_1_1(x#construct_double_2.1_1(xy), y#construct_double_2.1_1(xy), z)
}

function {:inline true} double_2_insert_0(v: double_2, x: double) : double_2
{
  construct_double_2.1_1(x, y#construct_double_2.1_1(v))
}

function {:inline true} double_2_insert_1(v: double_2, y: double) : double_2
{
  construct_double_2.1_1(x#construct_double_2.1_1(v), y)
}

function {:inline true} double_3_insert_0(v: double_3, x: double) : double_3
{
  construct_double_3.1_1_1(x, y#construct_double_3.1_1_1(v), z#construct_double_3.1_1_1(v))
}

function {:inline true} double_3_insert_1(v: double_3, y: double) : double_3
{
  construct_double_3.1_1_1(x#construct_double_3.1_1_1(v), y, z#construct_double_3.1_1_1(v))
}

function {:inline true} double_3_insert_2(v: double_3, z: double) : double_3
{
  construct_double_3.1_1_1(x#construct_double_3.1_1_1(v), y#construct_double_3.1_1_1(v), z)
}

function {:inline true} double_4_insert_0(v: double_4, x: double) : double_4
{
  construct_double_4.1_1_1_1(x, y#construct_double_4.1_1_1_1(v), z#construct_double_4.1_1_1_1(v), w#construct_double_4.1_1_1_1(v))
}

function {:inline true} double_4_insert_1(v: double_4, y: double) : double_4
{
  construct_double_4.1_1_1_1(x#construct_double_4.1_1_1_1(v), y, z#construct_double_4.1_1_1_1(v), w#construct_double_4.1_1_1_1(v))
}

function {:inline true} double_4_insert_2(v: double_4, z: double) : double_4
{
  construct_double_4.1_1_1_1(x#construct_double_4.1_1_1_1(v), y#construct_double_4.1_1_1_1(v), z, w#construct_double_4.1_1_1_1(v))
}

function {:inline true} double_4_insert_3(v: double_4, w: double) : double_4
{
  construct_double_4.1_1_1_1(x#construct_double_4.1_1_1_1(v), y#construct_double_4.1_1_1_1(v), z#construct_double_4.1_1_1_1(v), w)
}

function {:inline true} double_8_insert_0(v: double_8, s0: double) : double_8
{
  construct_double_8.1_1_1_1_1_1_1_1(s0, s1#construct_double_8.1_1_1_1_1_1_1_1(v), s2#construct_double_8.1_1_1_1_1_1_1_1(v), s3#construct_double_8.1_1_1_1_1_1_1_1(v), s4#construct_double_8.1_1_1_1_1_1_1_1(v), s5#construct_double_8.1_1_1_1_1_1_1_1(v), s6#construct_double_8.1_1_1_1_1_1_1_1(v), s7#construct_double_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} double_8_insert_1(v: double_8, s1: double) : double_8
{
  construct_double_8.1_1_1_1_1_1_1_1(s0#construct_double_8.1_1_1_1_1_1_1_1(v), s1, s2#construct_double_8.1_1_1_1_1_1_1_1(v), s3#construct_double_8.1_1_1_1_1_1_1_1(v), s4#construct_double_8.1_1_1_1_1_1_1_1(v), s5#construct_double_8.1_1_1_1_1_1_1_1(v), s6#construct_double_8.1_1_1_1_1_1_1_1(v), s7#construct_double_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} double_8_insert_2(v: double_8, s2: double) : double_8
{
  construct_double_8.1_1_1_1_1_1_1_1(s0#construct_double_8.1_1_1_1_1_1_1_1(v), s1#construct_double_8.1_1_1_1_1_1_1_1(v), s2, s3#construct_double_8.1_1_1_1_1_1_1_1(v), s4#construct_double_8.1_1_1_1_1_1_1_1(v), s5#construct_double_8.1_1_1_1_1_1_1_1(v), s6#construct_double_8.1_1_1_1_1_1_1_1(v), s7#construct_double_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} double_8_insert_3(v: double_8, s3: double) : double_8
{
  construct_double_8.1_1_1_1_1_1_1_1(s0#construct_double_8.1_1_1_1_1_1_1_1(v), s1#construct_double_8.1_1_1_1_1_1_1_1(v), s2#construct_double_8.1_1_1_1_1_1_1_1(v), s3, s4#construct_double_8.1_1_1_1_1_1_1_1(v), s5#construct_double_8.1_1_1_1_1_1_1_1(v), s6#construct_double_8.1_1_1_1_1_1_1_1(v), s7#construct_double_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} double_8_insert_4(v: double_8, s4: double) : double_8
{
  construct_double_8.1_1_1_1_1_1_1_1(s0#construct_double_8.1_1_1_1_1_1_1_1(v), s1#construct_double_8.1_1_1_1_1_1_1_1(v), s2#construct_double_8.1_1_1_1_1_1_1_1(v), s3#construct_double_8.1_1_1_1_1_1_1_1(v), s4, s5#construct_double_8.1_1_1_1_1_1_1_1(v), s6#construct_double_8.1_1_1_1_1_1_1_1(v), s7#construct_double_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} double_8_insert_5(v: double_8, s5: double) : double_8
{
  construct_double_8.1_1_1_1_1_1_1_1(s0#construct_double_8.1_1_1_1_1_1_1_1(v), s1#construct_double_8.1_1_1_1_1_1_1_1(v), s2#construct_double_8.1_1_1_1_1_1_1_1(v), s3#construct_double_8.1_1_1_1_1_1_1_1(v), s4#construct_double_8.1_1_1_1_1_1_1_1(v), s5, s6#construct_double_8.1_1_1_1_1_1_1_1(v), s7#construct_double_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} double_8_insert_6(v: double_8, s6: double) : double_8
{
  construct_double_8.1_1_1_1_1_1_1_1(s0#construct_double_8.1_1_1_1_1_1_1_1(v), s1#construct_double_8.1_1_1_1_1_1_1_1(v), s2#construct_double_8.1_1_1_1_1_1_1_1(v), s3#construct_double_8.1_1_1_1_1_1_1_1(v), s4#construct_double_8.1_1_1_1_1_1_1_1(v), s5#construct_double_8.1_1_1_1_1_1_1_1(v), s6, s7#construct_double_8.1_1_1_1_1_1_1_1(v))
}

function {:inline true} double_8_insert_7(v: double_8, s7: double) : double_8
{
  construct_double_8.1_1_1_1_1_1_1_1(s0#construct_double_8.1_1_1_1_1_1_1_1(v), s1#construct_double_8.1_1_1_1_1_1_1_1(v), s2#construct_double_8.1_1_1_1_1_1_1_1(v), s3#construct_double_8.1_1_1_1_1_1_1_1(v), s4#construct_double_8.1_1_1_1_1_1_1_1(v), s5#construct_double_8.1_1_1_1_1_1_1_1(v), s6#construct_double_8.1_1_1_1_1_1_1_1(v), s7)
}

function {:inline true} double_2_extract_0(v: double_2) : double
{
  x#construct_double_2.1_1(v)
}

function {:inline true} double_2_extract_1(v: double_2) : double
{
  y#construct_double_2.1_1(v)
}

function {:inline true} double_3_extract_0(v: double_3) : double
{
  x#construct_double_3.1_1_1(v)
}

function {:inline true} double_3_extract_1(v: double_3) : double
{
  y#construct_double_3.1_1_1(v)
}

function {:inline true} double_3_extract_2(v: double_3) : double
{
  z#construct_double_3.1_1_1(v)
}

function {:inline true} double_4_extract_0(v: double_4) : double
{
  x#construct_double_4.1_1_1_1(v)
}

function {:inline true} double_4_extract_1(v: double_4) : double
{
  y#construct_double_4.1_1_1_1(v)
}

function {:inline true} double_4_extract_2(v: double_4) : double
{
  z#construct_double_4.1_1_1_1(v)
}

function {:inline true} double_4_extract_3(v: double_4) : double
{
  w#construct_double_4.1_1_1_1(v)
}

function {:inline true} double_8_extract_0(v: double_8) : double
{
  s0#construct_double_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} double_8_extract_1(v: double_8) : double
{
  s1#construct_double_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} double_8_extract_2(v: double_8) : double
{
  s2#construct_double_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} double_8_extract_3(v: double_8) : double
{
  s3#construct_double_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} double_8_extract_4(v: double_8) : double
{
  s4#construct_double_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} double_8_extract_5(v: double_8) : double
{
  s5#construct_double_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} double_8_extract_6(v: double_8) : double
{
  s6#construct_double_8.1_1_1_1_1_1_1_1(v)
}

function {:inline true} double_8_extract_7(v: double_8) : double
{
  s7#construct_double_8.1_1_1_1_1_1_1_1(v)
}






















procedure {:inline 1} {:barrier} barrier(_P$1: bool, _P$2: bool);



function acos(float) : float;

function atan2(float, float) : float;

function cbrt_4(float_4) : float_4;

function convert_float4_ui(bv32_4) : float_4;

function convert_uint4(float_4) : bv32_4;

function cos(float) : float;

function cross_3(float_3, float_3) : float_3;

function cross_4(float_4, float_4) : float_4;

function dot_2(float_2, float_2) : float;

function dot_3(float_3, float_3) : float;

function dot_4(float_4, float_4) : float;

function fast_length_2(float_2) : float;

function fast_length_3(float_3) : float;

function fast_length_4(float_4) : float;

function fast_normalize_2(float_2) : float_2;

function fast_normalize_3(float_3) : float_3;

function fast_normalize_4(float_4) : float_4;

function floor(float) : float;

function half_cos(float) : float;

function half_exp(float) : float;

function half_exp_4(float_4) : float_4;

function half_log(float) : float;

function half_powr(float, float) : float;

function half_powr_4(float_4, float_4) : float_4;

function half_sin(float) : float;

function half_sqrt(float) : float;

function length_2(float_2) : float;

function length_3(float_3) : float;

function length_4(float_4) : float;

function log2(float) : float;

function max(float, float) : float;

function max_2(float_2, float_2) : float_2;

function max_3(float_3, float_3) : float_3;

function max_4(float_4, float_4) : float_4;

function min_2(float_2, float_2) : float_2;

function min_3(float_3, float_3) : float_3;

function min_4(float_4, float_4) : float_4;

function pow(float, float) : float;

function pown(float, bv32) : float;

function rsqrt(float) : float;

function sin(float) : float;

const {:local_id_x} get_local_id.0$1: bv32;

const {:local_id_x} get_local_id.0$2: bv32;

const {:group_id_x} get_group_id.0: bv32;

const {:group_size_x} get_local_size.0: bv32;

const {:num_groups_x} get_num_groups.0: bv32;

const {:local_id_y} get_local_id.1$1: bv32;

const {:local_id_y} get_local_id.1$2: bv32;

const {:group_id_y} get_group_id.1: bv32;

const {:group_size_y} get_local_size.1: bv32;

const {:num_groups_y} get_num_groups.1: bv32;

const {:local_id_z} get_local_id.2$1: bv32;

const {:local_id_z} get_local_id.2$2: bv32;

const {:group_id_z} get_group_id.2: bv32;

const {:group_size_z} get_local_size.2: bv32;

const {:num_groups_z} get_num_groups.2: bv32;

type image2d_t;

type image3d_t;

type pixel_t;

function pixel_to_float_4(pixel_t) : float_4;

function pixel_to_bv32_4(pixel_t) : bv32_4;

function float_4_to_pixel(float_4) : pixel_t;

function bv32_4_to_pixel(bv32_4) : pixel_t;

function get_image_height(image2d_t) : bv32;

function get_image_width(image2d_t) : bv32;

function {:inline true} __implies(p: bool, q: bool) : bool
{
  p ==> q
}

function __enabled() : bool;

function __uniform_bool(b: bool) : bool;

function __uniform_bv32(x: bv32) : bool;

function __distinct_bool(b: bool) : bool;

function __distinct_bv32(x: bv32) : bool;

function __all(x: bool) : bool;

function __at_most_one(x: bool) : bool;

var _READ_HAS_OCCURRED__ARRAY_if0$1: bool;

var _READ_OFFSET_X__ARRAY_if0$1: bv32;

var _WRITE_HAS_OCCURRED__ARRAY_if0$1: bool;

var _WRITE_HAS_OCCURRED__ARRAY_if0$2: bool;

var _WRITE_OFFSET_X__ARRAY_if0$1: bv32;

var _WRITE_OFFSET_X__ARRAY_if0$2: bv32;

procedure {:inline 1} _LOG_READ__ARRAY_if0(_P$1: bool, _X_index$1: bv32);
  modifies _READ_OFFSET_X__ARRAY_if0$1, _READ_HAS_OCCURRED__ARRAY_if0$1;



implementation {:inline 1} _LOG_READ__ARRAY_if0(_P$1: bool, _X_index$1: bv32)
{
  var track$1: bool;
  var _HAVOC_bool$1: bool;

  _LOG_READ:
    havoc _HAVOC_bool$1;
    track$1 := (if _P$1 then _HAVOC_bool$1 else track$1);
    _READ_HAS_OCCURRED__ARRAY_if0$1 := (if _P$1 then (if track$1 then true else _READ_HAS_OCCURRED__ARRAY_if0$1) else _READ_HAS_OCCURRED__ARRAY_if0$1);
    _READ_OFFSET_X__ARRAY_if0$1 := (if _P$1 then (if track$1 then _X_index$1 else _READ_OFFSET_X__ARRAY_if0$1) else _READ_OFFSET_X__ARRAY_if0$1);

  __CheckForRaces:
    assert !(_READ_HAS_OCCURRED__ARRAY_if0$1 && _WRITE_HAS_OCCURRED__ARRAY_if0$2 && _READ_OFFSET_X__ARRAY_if0$1 == _WRITE_OFFSET_X__ARRAY_if0$2);
}



procedure {:inline 1} _LOG_WRITE__ARRAY_if0(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32);
  modifies _WRITE_OFFSET_X__ARRAY_if0$1, _WRITE_HAS_OCCURRED__ARRAY_if0$1, _WRITE_OFFSET_X__ARRAY_if0$2, _WRITE_HAS_OCCURRED__ARRAY_if0$2;



implementation {:inline 1} _LOG_WRITE__ARRAY_if0(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32)
{
  var track$1: bool;
  var track$2: bool;
  var _HAVOC_bool$1: bool;
  var _HAVOC_bool$2: bool;

  _LOG_WRITE:
    havoc _HAVOC_bool$1, _HAVOC_bool$2;
    track$1, track$2 := (if _P$1 then _HAVOC_bool$1 else track$1), (if _P$2 then _HAVOC_bool$2 else track$2);
    _WRITE_HAS_OCCURRED__ARRAY_if0$1, _WRITE_HAS_OCCURRED__ARRAY_if0$2 := (if _P$1 then (if track$1 then true else _WRITE_HAS_OCCURRED__ARRAY_if0$1) else _WRITE_HAS_OCCURRED__ARRAY_if0$1), (if _P$2 then (if track$2 then true else _WRITE_HAS_OCCURRED__ARRAY_if0$2) else _WRITE_HAS_OCCURRED__ARRAY_if0$2);
    _WRITE_OFFSET_X__ARRAY_if0$1, _WRITE_OFFSET_X__ARRAY_if0$2 := (if _P$1 then (if track$1 then _X_index$1 else _WRITE_OFFSET_X__ARRAY_if0$1) else _WRITE_OFFSET_X__ARRAY_if0$1), (if _P$2 then (if track$2 then _X_index$2 else _WRITE_OFFSET_X__ARRAY_if0$2) else _WRITE_OFFSET_X__ARRAY_if0$2);

  __CheckForRaces:
    assert !(_WRITE_HAS_OCCURRED__ARRAY_if0$1 && _WRITE_HAS_OCCURRED__ARRAY_if0$2 && _WRITE_OFFSET_X__ARRAY_if0$1 == _WRITE_OFFSET_X__ARRAY_if0$2);
    assert !(_READ_HAS_OCCURRED__ARRAY_if0$1 && _WRITE_HAS_OCCURRED__ARRAY_if0$2 && _READ_OFFSET_X__ARRAY_if0$1 == _WRITE_OFFSET_X__ARRAY_if0$2);
}



var _READ_HAS_OCCURRED__ARRAY_of0$1: bool;

var _READ_OFFSET_X__ARRAY_of0$1: bv32;

var _WRITE_HAS_OCCURRED__ARRAY_of0$1: bool;

var _WRITE_HAS_OCCURRED__ARRAY_of0$2: bool;

var _WRITE_OFFSET_X__ARRAY_of0$1: bv32;

var _WRITE_OFFSET_X__ARRAY_of0$2: bv32;

procedure {:inline 1} _LOG_READ__ARRAY_of0(_P$1: bool, _X_index$1: bv32);
  modifies _READ_OFFSET_X__ARRAY_of0$1, _READ_HAS_OCCURRED__ARRAY_of0$1;



implementation {:inline 1} _LOG_READ__ARRAY_of0(_P$1: bool, _X_index$1: bv32)
{
  var track$1: bool;
  var _HAVOC_bool$1: bool;

  _LOG_READ:
    havoc _HAVOC_bool$1;
    track$1 := (if _P$1 then _HAVOC_bool$1 else track$1);
    _READ_HAS_OCCURRED__ARRAY_of0$1 := (if _P$1 then (if track$1 then true else _READ_HAS_OCCURRED__ARRAY_of0$1) else _READ_HAS_OCCURRED__ARRAY_of0$1);
    _READ_OFFSET_X__ARRAY_of0$1 := (if _P$1 then (if track$1 then _X_index$1 else _READ_OFFSET_X__ARRAY_of0$1) else _READ_OFFSET_X__ARRAY_of0$1);

  __CheckForRaces:
    assert !(_READ_HAS_OCCURRED__ARRAY_of0$1 && _WRITE_HAS_OCCURRED__ARRAY_of0$2 && _READ_OFFSET_X__ARRAY_of0$1 == _WRITE_OFFSET_X__ARRAY_of0$2);
}



procedure {:inline 1} _LOG_WRITE__ARRAY_of0(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32);
  modifies _WRITE_OFFSET_X__ARRAY_of0$1, _WRITE_HAS_OCCURRED__ARRAY_of0$1, _WRITE_OFFSET_X__ARRAY_of0$2, _WRITE_HAS_OCCURRED__ARRAY_of0$2;



implementation {:inline 1} _LOG_WRITE__ARRAY_of0(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32)
{
  var track$1: bool;
  var track$2: bool;
  var _HAVOC_bool$1: bool;
  var _HAVOC_bool$2: bool;

  _LOG_WRITE:
    havoc _HAVOC_bool$1, _HAVOC_bool$2;
    track$1, track$2 := (if _P$1 then _HAVOC_bool$1 else track$1), (if _P$2 then _HAVOC_bool$2 else track$2);
    _WRITE_HAS_OCCURRED__ARRAY_of0$1, _WRITE_HAS_OCCURRED__ARRAY_of0$2 := (if _P$1 then (if track$1 then true else _WRITE_HAS_OCCURRED__ARRAY_of0$1) else _WRITE_HAS_OCCURRED__ARRAY_of0$1), (if _P$2 then (if track$2 then true else _WRITE_HAS_OCCURRED__ARRAY_of0$2) else _WRITE_HAS_OCCURRED__ARRAY_of0$2);
    _WRITE_OFFSET_X__ARRAY_of0$1, _WRITE_OFFSET_X__ARRAY_of0$2 := (if _P$1 then (if track$1 then _X_index$1 else _WRITE_OFFSET_X__ARRAY_of0$1) else _WRITE_OFFSET_X__ARRAY_of0$1), (if _P$2 then (if track$2 then _X_index$2 else _WRITE_OFFSET_X__ARRAY_of0$2) else _WRITE_OFFSET_X__ARRAY_of0$2);

  __CheckForRaces:
    assert !(_WRITE_HAS_OCCURRED__ARRAY_of0$1 && _WRITE_HAS_OCCURRED__ARRAY_of0$2 && _WRITE_OFFSET_X__ARRAY_of0$1 == _WRITE_OFFSET_X__ARRAY_of0$2);
    assert !(_READ_HAS_OCCURRED__ARRAY_of0$1 && _WRITE_HAS_OCCURRED__ARRAY_of0$2 && _READ_OFFSET_X__ARRAY_of0$1 == _WRITE_OFFSET_X__ARRAY_of0$2);
}



var _READ_HAS_OCCURRED__ARRAY_if1234$1: bool;

var _READ_OFFSET_X__ARRAY_if1234$1: bv32;

var _WRITE_HAS_OCCURRED__ARRAY_if1234$1: bool;

var _WRITE_HAS_OCCURRED__ARRAY_if1234$2: bool;

var _WRITE_OFFSET_X__ARRAY_if1234$1: bv32;

var _WRITE_OFFSET_X__ARRAY_if1234$2: bv32;

procedure {:inline 1} _LOG_READ__ARRAY_if1234(_P$1: bool, _X_index$1: bv32);
  modifies _READ_OFFSET_X__ARRAY_if1234$1, _READ_HAS_OCCURRED__ARRAY_if1234$1;



implementation {:inline 1} _LOG_READ__ARRAY_if1234(_P$1: bool, _X_index$1: bv32)
{
  var track$1: bool;
  var _HAVOC_bool$1: bool;

  _LOG_READ:
    havoc _HAVOC_bool$1;
    track$1 := (if _P$1 then _HAVOC_bool$1 else track$1);
    _READ_HAS_OCCURRED__ARRAY_if1234$1 := (if _P$1 then (if track$1 then true else _READ_HAS_OCCURRED__ARRAY_if1234$1) else _READ_HAS_OCCURRED__ARRAY_if1234$1);
    _READ_OFFSET_X__ARRAY_if1234$1 := (if _P$1 then (if track$1 then _X_index$1 else _READ_OFFSET_X__ARRAY_if1234$1) else _READ_OFFSET_X__ARRAY_if1234$1);

  __CheckForRaces:
    assert !(_READ_HAS_OCCURRED__ARRAY_if1234$1 && _WRITE_HAS_OCCURRED__ARRAY_if1234$2 && _READ_OFFSET_X__ARRAY_if1234$1 == _WRITE_OFFSET_X__ARRAY_if1234$2);
}



procedure {:inline 1} _LOG_WRITE__ARRAY_if1234(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32);
  modifies _WRITE_OFFSET_X__ARRAY_if1234$1, _WRITE_HAS_OCCURRED__ARRAY_if1234$1, _WRITE_OFFSET_X__ARRAY_if1234$2, _WRITE_HAS_OCCURRED__ARRAY_if1234$2;



implementation {:inline 1} _LOG_WRITE__ARRAY_if1234(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32)
{
  var track$1: bool;
  var track$2: bool;
  var _HAVOC_bool$1: bool;
  var _HAVOC_bool$2: bool;

  _LOG_WRITE:
    havoc _HAVOC_bool$1, _HAVOC_bool$2;
    track$1, track$2 := (if _P$1 then _HAVOC_bool$1 else track$1), (if _P$2 then _HAVOC_bool$2 else track$2);
    _WRITE_HAS_OCCURRED__ARRAY_if1234$1, _WRITE_HAS_OCCURRED__ARRAY_if1234$2 := (if _P$1 then (if track$1 then true else _WRITE_HAS_OCCURRED__ARRAY_if1234$1) else _WRITE_HAS_OCCURRED__ARRAY_if1234$1), (if _P$2 then (if track$2 then true else _WRITE_HAS_OCCURRED__ARRAY_if1234$2) else _WRITE_HAS_OCCURRED__ARRAY_if1234$2);
    _WRITE_OFFSET_X__ARRAY_if1234$1, _WRITE_OFFSET_X__ARRAY_if1234$2 := (if _P$1 then (if track$1 then _X_index$1 else _WRITE_OFFSET_X__ARRAY_if1234$1) else _WRITE_OFFSET_X__ARRAY_if1234$1), (if _P$2 then (if track$2 then _X_index$2 else _WRITE_OFFSET_X__ARRAY_if1234$2) else _WRITE_OFFSET_X__ARRAY_if1234$2);

  __CheckForRaces:
    assert !(_WRITE_HAS_OCCURRED__ARRAY_if1234$1 && _WRITE_HAS_OCCURRED__ARRAY_if1234$2 && _WRITE_OFFSET_X__ARRAY_if1234$1 == _WRITE_OFFSET_X__ARRAY_if1234$2);
    assert !(_READ_HAS_OCCURRED__ARRAY_if1234$1 && _WRITE_HAS_OCCURRED__ARRAY_if1234$2 && _READ_OFFSET_X__ARRAY_if1234$1 == _WRITE_OFFSET_X__ARRAY_if1234$2);
}



var _READ_HAS_OCCURRED__ARRAY_of1234$1: bool;

var _READ_OFFSET_X__ARRAY_of1234$1: bv32;

var _WRITE_HAS_OCCURRED__ARRAY_of1234$1: bool;

var _WRITE_HAS_OCCURRED__ARRAY_of1234$2: bool;

var _WRITE_OFFSET_X__ARRAY_of1234$1: bv32;

var _WRITE_OFFSET_X__ARRAY_of1234$2: bv32;

procedure {:inline 1} _LOG_READ__ARRAY_of1234(_P$1: bool, _X_index$1: bv32);
  modifies _READ_OFFSET_X__ARRAY_of1234$1, _READ_HAS_OCCURRED__ARRAY_of1234$1;



implementation {:inline 1} _LOG_READ__ARRAY_of1234(_P$1: bool, _X_index$1: bv32)
{
  var track$1: bool;
  var _HAVOC_bool$1: bool;

  _LOG_READ:
    havoc _HAVOC_bool$1;
    track$1 := (if _P$1 then _HAVOC_bool$1 else track$1);
    _READ_HAS_OCCURRED__ARRAY_of1234$1 := (if _P$1 then (if track$1 then true else _READ_HAS_OCCURRED__ARRAY_of1234$1) else _READ_HAS_OCCURRED__ARRAY_of1234$1);
    _READ_OFFSET_X__ARRAY_of1234$1 := (if _P$1 then (if track$1 then _X_index$1 else _READ_OFFSET_X__ARRAY_of1234$1) else _READ_OFFSET_X__ARRAY_of1234$1);

  __CheckForRaces:
    assert !(_READ_HAS_OCCURRED__ARRAY_of1234$1 && _WRITE_HAS_OCCURRED__ARRAY_of1234$2 && _READ_OFFSET_X__ARRAY_of1234$1 == _WRITE_OFFSET_X__ARRAY_of1234$2);
}



procedure {:inline 1} _LOG_WRITE__ARRAY_of1234(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32);
  modifies _WRITE_OFFSET_X__ARRAY_of1234$1, _WRITE_HAS_OCCURRED__ARRAY_of1234$1, _WRITE_OFFSET_X__ARRAY_of1234$2, _WRITE_HAS_OCCURRED__ARRAY_of1234$2;



implementation {:inline 1} _LOG_WRITE__ARRAY_of1234(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32)
{
  var track$1: bool;
  var track$2: bool;
  var _HAVOC_bool$1: bool;
  var _HAVOC_bool$2: bool;

  _LOG_WRITE:
    havoc _HAVOC_bool$1, _HAVOC_bool$2;
    track$1, track$2 := (if _P$1 then _HAVOC_bool$1 else track$1), (if _P$2 then _HAVOC_bool$2 else track$2);
    _WRITE_HAS_OCCURRED__ARRAY_of1234$1, _WRITE_HAS_OCCURRED__ARRAY_of1234$2 := (if _P$1 then (if track$1 then true else _WRITE_HAS_OCCURRED__ARRAY_of1234$1) else _WRITE_HAS_OCCURRED__ARRAY_of1234$1), (if _P$2 then (if track$2 then true else _WRITE_HAS_OCCURRED__ARRAY_of1234$2) else _WRITE_HAS_OCCURRED__ARRAY_of1234$2);
    _WRITE_OFFSET_X__ARRAY_of1234$1, _WRITE_OFFSET_X__ARRAY_of1234$2 := (if _P$1 then (if track$1 then _X_index$1 else _WRITE_OFFSET_X__ARRAY_of1234$1) else _WRITE_OFFSET_X__ARRAY_of1234$1), (if _P$2 then (if track$2 then _X_index$2 else _WRITE_OFFSET_X__ARRAY_of1234$2) else _WRITE_OFFSET_X__ARRAY_of1234$2);

  __CheckForRaces:
    assert !(_WRITE_HAS_OCCURRED__ARRAY_of1234$1 && _WRITE_HAS_OCCURRED__ARRAY_of1234$2 && _WRITE_OFFSET_X__ARRAY_of1234$1 == _WRITE_OFFSET_X__ARRAY_of1234$2);
    assert !(_READ_HAS_OCCURRED__ARRAY_of1234$1 && _WRITE_HAS_OCCURRED__ARRAY_of1234$2 && _READ_OFFSET_X__ARRAY_of1234$1 == _WRITE_OFFSET_X__ARRAY_of1234$2);
}



var _READ_HAS_OCCURRED__ARRAY_if5678$1: bool;

var _READ_OFFSET_X__ARRAY_if5678$1: bv32;

var _WRITE_HAS_OCCURRED__ARRAY_if5678$1: bool;

var _WRITE_HAS_OCCURRED__ARRAY_if5678$2: bool;

var _WRITE_OFFSET_X__ARRAY_if5678$1: bv32;

var _WRITE_OFFSET_X__ARRAY_if5678$2: bv32;

procedure {:inline 1} _LOG_READ__ARRAY_if5678(_P$1: bool, _X_index$1: bv32);
  modifies _READ_OFFSET_X__ARRAY_if5678$1, _READ_HAS_OCCURRED__ARRAY_if5678$1;



implementation {:inline 1} _LOG_READ__ARRAY_if5678(_P$1: bool, _X_index$1: bv32)
{
  var track$1: bool;
  var _HAVOC_bool$1: bool;

  _LOG_READ:
    havoc _HAVOC_bool$1;
    track$1 := (if _P$1 then _HAVOC_bool$1 else track$1);
    _READ_HAS_OCCURRED__ARRAY_if5678$1 := (if _P$1 then (if track$1 then true else _READ_HAS_OCCURRED__ARRAY_if5678$1) else _READ_HAS_OCCURRED__ARRAY_if5678$1);
    _READ_OFFSET_X__ARRAY_if5678$1 := (if _P$1 then (if track$1 then _X_index$1 else _READ_OFFSET_X__ARRAY_if5678$1) else _READ_OFFSET_X__ARRAY_if5678$1);

  __CheckForRaces:
    assert !(_READ_HAS_OCCURRED__ARRAY_if5678$1 && _WRITE_HAS_OCCURRED__ARRAY_if5678$2 && _READ_OFFSET_X__ARRAY_if5678$1 == _WRITE_OFFSET_X__ARRAY_if5678$2);
}



procedure {:inline 1} _LOG_WRITE__ARRAY_if5678(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32);
  modifies _WRITE_OFFSET_X__ARRAY_if5678$1, _WRITE_HAS_OCCURRED__ARRAY_if5678$1, _WRITE_OFFSET_X__ARRAY_if5678$2, _WRITE_HAS_OCCURRED__ARRAY_if5678$2;



implementation {:inline 1} _LOG_WRITE__ARRAY_if5678(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32)
{
  var track$1: bool;
  var track$2: bool;
  var _HAVOC_bool$1: bool;
  var _HAVOC_bool$2: bool;

  _LOG_WRITE:
    havoc _HAVOC_bool$1, _HAVOC_bool$2;
    track$1, track$2 := (if _P$1 then _HAVOC_bool$1 else track$1), (if _P$2 then _HAVOC_bool$2 else track$2);
    _WRITE_HAS_OCCURRED__ARRAY_if5678$1, _WRITE_HAS_OCCURRED__ARRAY_if5678$2 := (if _P$1 then (if track$1 then true else _WRITE_HAS_OCCURRED__ARRAY_if5678$1) else _WRITE_HAS_OCCURRED__ARRAY_if5678$1), (if _P$2 then (if track$2 then true else _WRITE_HAS_OCCURRED__ARRAY_if5678$2) else _WRITE_HAS_OCCURRED__ARRAY_if5678$2);
    _WRITE_OFFSET_X__ARRAY_if5678$1, _WRITE_OFFSET_X__ARRAY_if5678$2 := (if _P$1 then (if track$1 then _X_index$1 else _WRITE_OFFSET_X__ARRAY_if5678$1) else _WRITE_OFFSET_X__ARRAY_if5678$1), (if _P$2 then (if track$2 then _X_index$2 else _WRITE_OFFSET_X__ARRAY_if5678$2) else _WRITE_OFFSET_X__ARRAY_if5678$2);

  __CheckForRaces:
    assert !(_WRITE_HAS_OCCURRED__ARRAY_if5678$1 && _WRITE_HAS_OCCURRED__ARRAY_if5678$2 && _WRITE_OFFSET_X__ARRAY_if5678$1 == _WRITE_OFFSET_X__ARRAY_if5678$2);
    assert !(_READ_HAS_OCCURRED__ARRAY_if5678$1 && _WRITE_HAS_OCCURRED__ARRAY_if5678$2 && _READ_OFFSET_X__ARRAY_if5678$1 == _WRITE_OFFSET_X__ARRAY_if5678$2);
}



var _READ_HAS_OCCURRED__ARRAY_of5678$1: bool;

var _READ_OFFSET_X__ARRAY_of5678$1: bv32;

var _WRITE_HAS_OCCURRED__ARRAY_of5678$1: bool;

var _WRITE_HAS_OCCURRED__ARRAY_of5678$2: bool;

var _WRITE_OFFSET_X__ARRAY_of5678$1: bv32;

var _WRITE_OFFSET_X__ARRAY_of5678$2: bv32;

procedure {:inline 1} _LOG_READ__ARRAY_of5678(_P$1: bool, _X_index$1: bv32);
  modifies _READ_OFFSET_X__ARRAY_of5678$1, _READ_HAS_OCCURRED__ARRAY_of5678$1;



implementation {:inline 1} _LOG_READ__ARRAY_of5678(_P$1: bool, _X_index$1: bv32)
{
  var track$1: bool;
  var _HAVOC_bool$1: bool;

  _LOG_READ:
    havoc _HAVOC_bool$1;
    track$1 := (if _P$1 then _HAVOC_bool$1 else track$1);
    _READ_HAS_OCCURRED__ARRAY_of5678$1 := (if _P$1 then (if track$1 then true else _READ_HAS_OCCURRED__ARRAY_of5678$1) else _READ_HAS_OCCURRED__ARRAY_of5678$1);
    _READ_OFFSET_X__ARRAY_of5678$1 := (if _P$1 then (if track$1 then _X_index$1 else _READ_OFFSET_X__ARRAY_of5678$1) else _READ_OFFSET_X__ARRAY_of5678$1);

  __CheckForRaces:
    assert !(_READ_HAS_OCCURRED__ARRAY_of5678$1 && _WRITE_HAS_OCCURRED__ARRAY_of5678$2 && _READ_OFFSET_X__ARRAY_of5678$1 == _WRITE_OFFSET_X__ARRAY_of5678$2);
}



procedure {:inline 1} _LOG_WRITE__ARRAY_of5678(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32);
  modifies _WRITE_OFFSET_X__ARRAY_of5678$1, _WRITE_HAS_OCCURRED__ARRAY_of5678$1, _WRITE_OFFSET_X__ARRAY_of5678$2, _WRITE_HAS_OCCURRED__ARRAY_of5678$2;



implementation {:inline 1} _LOG_WRITE__ARRAY_of5678(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32)
{
  var track$1: bool;
  var track$2: bool;
  var _HAVOC_bool$1: bool;
  var _HAVOC_bool$2: bool;

  _LOG_WRITE:
    havoc _HAVOC_bool$1, _HAVOC_bool$2;
    track$1, track$2 := (if _P$1 then _HAVOC_bool$1 else track$1), (if _P$2 then _HAVOC_bool$2 else track$2);
    _WRITE_HAS_OCCURRED__ARRAY_of5678$1, _WRITE_HAS_OCCURRED__ARRAY_of5678$2 := (if _P$1 then (if track$1 then true else _WRITE_HAS_OCCURRED__ARRAY_of5678$1) else _WRITE_HAS_OCCURRED__ARRAY_of5678$1), (if _P$2 then (if track$2 then true else _WRITE_HAS_OCCURRED__ARRAY_of5678$2) else _WRITE_HAS_OCCURRED__ARRAY_of5678$2);
    _WRITE_OFFSET_X__ARRAY_of5678$1, _WRITE_OFFSET_X__ARRAY_of5678$2 := (if _P$1 then (if track$1 then _X_index$1 else _WRITE_OFFSET_X__ARRAY_of5678$1) else _WRITE_OFFSET_X__ARRAY_of5678$1), (if _P$2 then (if track$2 then _X_index$2 else _WRITE_OFFSET_X__ARRAY_of5678$2) else _WRITE_OFFSET_X__ARRAY_of5678$2);

  __CheckForRaces:
    assert !(_WRITE_HAS_OCCURRED__ARRAY_of5678$1 && _WRITE_HAS_OCCURRED__ARRAY_of5678$2 && _WRITE_OFFSET_X__ARRAY_of5678$1 == _WRITE_OFFSET_X__ARRAY_of5678$2);
    assert !(_READ_HAS_OCCURRED__ARRAY_of5678$1 && _WRITE_HAS_OCCURRED__ARRAY_of5678$2 && _READ_OFFSET_X__ARRAY_of5678$1 == _WRITE_OFFSET_X__ARRAY_of5678$2);
}



var _READ_HAS_OCCURRED__ARRAY_typeVar$1: bool;

var _READ_OFFSET_X__ARRAY_typeVar$1: bv32;

var _WRITE_HAS_OCCURRED__ARRAY_typeVar$1: bool;

var _WRITE_HAS_OCCURRED__ARRAY_typeVar$2: bool;

var _WRITE_OFFSET_X__ARRAY_typeVar$1: bv32;

var _WRITE_OFFSET_X__ARRAY_typeVar$2: bv32;

procedure {:inline 1} _LOG_READ__ARRAY_typeVar(_P$1: bool, _X_index$1: bv32);
  modifies _READ_OFFSET_X__ARRAY_typeVar$1, _READ_HAS_OCCURRED__ARRAY_typeVar$1;



implementation {:inline 1} _LOG_READ__ARRAY_typeVar(_P$1: bool, _X_index$1: bv32)
{
  var track$1: bool;
  var _HAVOC_bool$1: bool;

  _LOG_READ:
    havoc _HAVOC_bool$1;
    track$1 := (if _P$1 then _HAVOC_bool$1 else track$1);
    _READ_HAS_OCCURRED__ARRAY_typeVar$1 := (if _P$1 then (if track$1 then true else _READ_HAS_OCCURRED__ARRAY_typeVar$1) else _READ_HAS_OCCURRED__ARRAY_typeVar$1);
    _READ_OFFSET_X__ARRAY_typeVar$1 := (if _P$1 then (if track$1 then _X_index$1 else _READ_OFFSET_X__ARRAY_typeVar$1) else _READ_OFFSET_X__ARRAY_typeVar$1);

  __CheckForRaces:
    assert !(_READ_HAS_OCCURRED__ARRAY_typeVar$1 && _WRITE_HAS_OCCURRED__ARRAY_typeVar$2 && _READ_OFFSET_X__ARRAY_typeVar$1 == _WRITE_OFFSET_X__ARRAY_typeVar$2);
}



procedure {:inline 1} _LOG_WRITE__ARRAY_typeVar(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32);
  modifies _WRITE_OFFSET_X__ARRAY_typeVar$1, _WRITE_HAS_OCCURRED__ARRAY_typeVar$1, _WRITE_OFFSET_X__ARRAY_typeVar$2, _WRITE_HAS_OCCURRED__ARRAY_typeVar$2;



implementation {:inline 1} _LOG_WRITE__ARRAY_typeVar(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32)
{
  var track$1: bool;
  var track$2: bool;
  var _HAVOC_bool$1: bool;
  var _HAVOC_bool$2: bool;

  _LOG_WRITE:
    havoc _HAVOC_bool$1, _HAVOC_bool$2;
    track$1, track$2 := (if _P$1 then _HAVOC_bool$1 else track$1), (if _P$2 then _HAVOC_bool$2 else track$2);
    _WRITE_HAS_OCCURRED__ARRAY_typeVar$1, _WRITE_HAS_OCCURRED__ARRAY_typeVar$2 := (if _P$1 then (if track$1 then true else _WRITE_HAS_OCCURRED__ARRAY_typeVar$1) else _WRITE_HAS_OCCURRED__ARRAY_typeVar$1), (if _P$2 then (if track$2 then true else _WRITE_HAS_OCCURRED__ARRAY_typeVar$2) else _WRITE_HAS_OCCURRED__ARRAY_typeVar$2);
    _WRITE_OFFSET_X__ARRAY_typeVar$1, _WRITE_OFFSET_X__ARRAY_typeVar$2 := (if _P$1 then (if track$1 then _X_index$1 else _WRITE_OFFSET_X__ARRAY_typeVar$1) else _WRITE_OFFSET_X__ARRAY_typeVar$1), (if _P$2 then (if track$2 then _X_index$2 else _WRITE_OFFSET_X__ARRAY_typeVar$2) else _WRITE_OFFSET_X__ARRAY_typeVar$2);

  __CheckForRaces:
    assert !(_WRITE_HAS_OCCURRED__ARRAY_typeVar$1 && _WRITE_HAS_OCCURRED__ARRAY_typeVar$2 && _WRITE_OFFSET_X__ARRAY_typeVar$1 == _WRITE_OFFSET_X__ARRAY_typeVar$2 && _ARRAY_typeVar$1[_WRITE_OFFSET_X__ARRAY_typeVar$1] != _ARRAY_typeVar$2[_WRITE_OFFSET_X__ARRAY_typeVar$2]);
    assert !(_READ_HAS_OCCURRED__ARRAY_typeVar$1 && _WRITE_HAS_OCCURRED__ARRAY_typeVar$2 && _READ_OFFSET_X__ARRAY_typeVar$1 == _WRITE_OFFSET_X__ARRAY_typeVar$2);
}



var _READ_HAS_OCCURRED__ARRAY_velocityBuffer$1: bool;

var _READ_OFFSET_X__ARRAY_velocityBuffer$1: bv32;

var _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$1: bool;

var _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$2: bool;

var _WRITE_OFFSET_X__ARRAY_velocityBuffer$1: bv32;

var _WRITE_OFFSET_X__ARRAY_velocityBuffer$2: bv32;

procedure {:inline 1} _LOG_READ__ARRAY_velocityBuffer(_P$1: bool, _X_index$1: bv32);
  modifies _READ_OFFSET_X__ARRAY_velocityBuffer$1, _READ_HAS_OCCURRED__ARRAY_velocityBuffer$1;



implementation {:inline 1} _LOG_READ__ARRAY_velocityBuffer(_P$1: bool, _X_index$1: bv32)
{
  var track$1: bool;
  var _HAVOC_bool$1: bool;

  _LOG_READ:
    havoc _HAVOC_bool$1;
    track$1 := (if _P$1 then _HAVOC_bool$1 else track$1);
    _READ_HAS_OCCURRED__ARRAY_velocityBuffer$1 := (if _P$1 then (if track$1 then true else _READ_HAS_OCCURRED__ARRAY_velocityBuffer$1) else _READ_HAS_OCCURRED__ARRAY_velocityBuffer$1);
    _READ_OFFSET_X__ARRAY_velocityBuffer$1 := (if _P$1 then (if track$1 then _X_index$1 else _READ_OFFSET_X__ARRAY_velocityBuffer$1) else _READ_OFFSET_X__ARRAY_velocityBuffer$1);

  __CheckForRaces:
    assert !(_READ_HAS_OCCURRED__ARRAY_velocityBuffer$1 && _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$2 && _READ_OFFSET_X__ARRAY_velocityBuffer$1 == _WRITE_OFFSET_X__ARRAY_velocityBuffer$2);
}



procedure {:inline 1} _LOG_WRITE__ARRAY_velocityBuffer(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32);
  modifies _WRITE_OFFSET_X__ARRAY_velocityBuffer$1, _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$1, _WRITE_OFFSET_X__ARRAY_velocityBuffer$2, _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$2;



implementation {:inline 1} _LOG_WRITE__ARRAY_velocityBuffer(_P$1: bool, _X_index$1: bv32, _P$2: bool, _X_index$2: bv32)
{
  var track$1: bool;
  var track$2: bool;
  var _HAVOC_bool$1: bool;
  var _HAVOC_bool$2: bool;

  _LOG_WRITE:
    havoc _HAVOC_bool$1, _HAVOC_bool$2;
    track$1, track$2 := (if _P$1 then _HAVOC_bool$1 else track$1), (if _P$2 then _HAVOC_bool$2 else track$2);
    _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$1, _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$2 := (if _P$1 then (if track$1 then true else _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$1) else _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$1), (if _P$2 then (if track$2 then true else _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$2) else _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$2);
    _WRITE_OFFSET_X__ARRAY_velocityBuffer$1, _WRITE_OFFSET_X__ARRAY_velocityBuffer$2 := (if _P$1 then (if track$1 then _X_index$1 else _WRITE_OFFSET_X__ARRAY_velocityBuffer$1) else _WRITE_OFFSET_X__ARRAY_velocityBuffer$1), (if _P$2 then (if track$2 then _X_index$2 else _WRITE_OFFSET_X__ARRAY_velocityBuffer$2) else _WRITE_OFFSET_X__ARRAY_velocityBuffer$2);

  __CheckForRaces:
    assert !(_WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$1 && _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$2 && _WRITE_OFFSET_X__ARRAY_velocityBuffer$1 == _WRITE_OFFSET_X__ARRAY_velocityBuffer$2);
    assert !(_READ_HAS_OCCURRED__ARRAY_velocityBuffer$1 && _WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$2 && _READ_OFFSET_X__ARRAY_velocityBuffer$1 == _WRITE_OFFSET_X__ARRAY_velocityBuffer$2);
}



implementation {:inline 1} barrier(_P$1: bool, _P$2: bool)
{
  __BarrierImpl:
    assert _P$1 == _P$2;
    if (!_P$1 || !_P$2)
    {
      __Disabled:
        return;
    }

  __CheckForRaces:
    assume !_READ_HAS_OCCURRED__ARRAY_if0$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_if0$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_if0$2;
    assume !_READ_HAS_OCCURRED__ARRAY_of0$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_of0$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_of0$2;
    assume !_READ_HAS_OCCURRED__ARRAY_if1234$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_if1234$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_if1234$2;
    assume !_READ_HAS_OCCURRED__ARRAY_of1234$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_of1234$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_of1234$2;
    assume !_READ_HAS_OCCURRED__ARRAY_if5678$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_if5678$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_if5678$2;
    assume !_READ_HAS_OCCURRED__ARRAY_of5678$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_of5678$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_of5678$2;
    assume !_READ_HAS_OCCURRED__ARRAY_typeVar$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_typeVar$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_typeVar$2;
    assume !_READ_HAS_OCCURRED__ARRAY_velocityBuffer$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$1;
    assume !_WRITE_HAS_OCCURRED__ARRAY_velocityBuffer$2;

  __HavocSharedState:
    havoc _ARRAY_typeVar$1, _ARRAY_typeVar$2;
    assume _ARRAY_typeVar$1 == _ARRAY_typeVar$2;
}


