(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Parametric timed pattern matching benchmark: accel
 *
 * Description     : Parametric timed pattern matching benchmark: accel
 * Correctness     : N/A
 * Source          : Benchmarks for Temporal Logic Requirements for Automotive Systems (ARCH@CPSWeek 2014) + Masaki Waga / Étienne André, Ichiro Husuo, Masaki Waga "Offline timed pattern matching under uncertainty" (ICECCS 2018)
 * Author          : The same
 * Modeling        : Étienne André
 * Input by        : Étienne André
 * License         : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 *
 * Created         : 2018/03/30
 * Last modified   : 2020/08/18
 *
 * IMITATOR version: 3
 ************************************************************)

var

(* Clocks *)
 	x, xabs
		: clock;

(* Parameters *)
	p10, t, tprime
		: parameter;

(*
MEANING OF THE EVENTS
* A: the gear changed to 1
* B: the gear changed to 2
* C: the gear changed to 3
* D: the gear changed to 4
* E: the rotation is low ($\omega < 2500$)
* F: the rotation is high ($\omega \ge 2500$)
* G: the velocity is low ($v < 100$)
* H: the velocity is high ($v \ge 100)
*)

(************************************************************)
  automaton pta
(************************************************************)
synclabs: A, B, C, D, E, F, G, H, dollar, start;

loc pre_s0: invariant True
	(* First try immediately the pattern in 0-time *)
	when xabs = 0 & xabs = t sync start goto pat_0;
	(* Otherwise: first skip some letter and wait *)
	when True sync A do {x := 0} goto pre_s0_prime;
	when True sync B do {x := 0} goto pre_s0_prime;
	when True sync C do {x := 0} goto pre_s0_prime;
	when True sync D do {x := 0} goto pre_s0_prime;
	when True sync E do {x := 0} goto pre_s0_prime;
	when True sync F do {x := 0} goto pre_s0_prime;
	when True sync G do {x := 0} goto pre_s0_prime;
	when True sync H do {x := 0} goto pre_s0_prime;

loc pre_s0_prime: invariant True
	(* Skip some more letter and wait *)
	when True sync A do {x := 0} goto pre_s0_prime;
	when True sync B do {x := 0} goto pre_s0_prime;
	when True sync C do {x := 0} goto pre_s0_prime;
	when True sync D do {x := 0} goto pre_s0_prime;
	when True sync E do {x := 0} goto pre_s0_prime;
	when True sync F do {x := 0} goto pre_s0_prime;
	when True sync G do {x := 0} goto pre_s0_prime;
	when True sync H do {x := 0} goto pre_s0_prime;
	(* Or decide to start the pattern *)
	when t = xabs & x > 0 do {x := 0} sync start goto pat_0;

loc pat_0: invariant True
	when True sync A (* g1 *) goto pat_g1;
	when True sync F (* rpmHigh *) goto pat_unknown;

loc pat_unknown: invariant True
	when True sync A (* g1 *) goto pat_g1_bis;

loc pat_g1: invariant True
	when True sync B (* g2 *) goto pat_g2;
	when True sync F (* rpmHigh *) goto pat_g1_bis;

loc pat_g1_bis: invariant True
	when True sync B (* g2 *) goto pat_g2_bis;

loc pat_g2: invariant True
	when True sync C (* g3 *) goto pat_g3;
	when True sync F (* rpmHigh *) goto pat_g2_bis;

loc pat_g2_bis: invariant True
	when True sync C (* g3 *) goto pat_g3_bis;

loc pat_g3: invariant True
	when x <= p10 do {x := 0} sync D (* g4 *) goto pat_g4;
	when True sync F (* rpmHigh *) goto pat_g3_bis;

loc pat_g3_bis: invariant True
	when x <= p10 do {x := 0} sync D (* g4 *) goto pat_g4_bis;

loc pat_g4: invariant True
	when True sync F (* rpmHigh *) goto pat_g4_bis;

loc pat_g4_bis: invariant True
	when tprime = xabs & x > 1 do {x := 0} sync dollar goto s_soon_end;

loc s_soon_end: invariant True
	when x > 0 goto s_end;

(* urgent to avoid time elapsing *)
urgent loc s_end: invariant True

end (* pta *)


(************************************************************)
  automaton word
(************************************************************)
synclabs: A, B, C, D, E, F, G, H;

	loc w1: invariant xabs <= 0.4
		when xabs = 0.4 sync A goto w2;
	loc w2: invariant xabs <= 2.32
		when xabs = 2.32 sync F goto w3;
	loc w3: invariant xabs <= 4.52
		when xabs = 4.52 sync B goto w4;
	loc w4: invariant xabs <= 9.64
		when xabs = 9.64 sync C goto w5;
	loc w5: invariant xabs <= 9.72
		when xabs = 9.72 sync H goto w6;
	loc w6: invariant xabs <= 18
		when xabs = 18 sync D goto w7;
	loc w7: invariant xabs <= 18.08
		when xabs = 18.08 sync E goto w8;
	loc w8: invariant xabs <= 18.28
		when xabs = 18.28 sync G goto w9;
	loc w9: invariant xabs <= 18.4
		when xabs = 18.4 sync C goto w10;
	loc w10: invariant xabs <= 18.52
		when xabs = 18.52 sync B goto w11;
	loc w11: invariant xabs <= 20.56
		when xabs = 20.56 sync A goto w12;
	loc w12: invariant xabs <= 21.6
		when xabs = 21.6 sync F goto w13;
	loc w13: invariant xabs <= 23.12
		when xabs = 23.12 sync B goto w14;
	loc w14: invariant xabs <= 27
		when xabs = 27 sync C goto w15;
	loc w15: invariant xabs <= 27.08
		when xabs = 27.08 sync H goto w16;
	loc w16: invariant xabs <= 38
		when xabs = 38 sync D goto w17;
	loc w17: invariant xabs <= 38.12
		when xabs = 38.12 sync E goto w18;
	loc w18: invariant xabs <= 38.32
		when xabs = 38.32 sync G goto w19;
	loc w19: invariant xabs <= 38.44
		when xabs = 38.44 sync C goto w20;
	loc w20: invariant xabs <= 38.56
		when xabs = 38.56 sync B goto w21;
	loc w21: invariant xabs <= 40.4
		when xabs = 40.4 sync A goto w22;
	loc w22: invariant xabs <= 41.12
		when xabs = 41.12 sync F goto w23;
	loc w23: invariant xabs <= 42.48
		when xabs = 42.48 sync B goto w24;
	loc w24: invariant xabs <= 45.24
		when xabs = 45.24 sync C goto w25;
	loc w25: invariant xabs <= 45.32
		when xabs = 45.32 sync H goto w26;
	loc w26: invariant xabs <= 58
		when xabs = 58 sync D goto w27;
	loc w27: invariant xabs <= 58.12
		when xabs = 58.12 sync E goto w28;
	loc w28: invariant xabs <= 58.32
		when xabs = 58.32 sync G goto w29;
	loc w29: invariant xabs <= 58.44
		when xabs = 58.44 sync C goto w30;
	loc w30: invariant xabs <= 58.56
		when xabs = 58.56 sync B goto w31;
	loc w31: invariant xabs <= 60.4
		when xabs = 60.4 sync A goto w32;
	loc w32: invariant xabs <= 61.32
		when xabs = 61.32 sync F goto w33;
	loc w33: invariant xabs <= 63.24
		when xabs = 63.24 sync B goto w34;
	loc w34: invariant xabs <= 66
		when xabs = 66 sync C goto w35;
	loc w35: invariant xabs <= 66.08
		when xabs = 66.08 sync H goto w36;
	loc w36: invariant xabs <= 78
		when xabs = 78 sync D goto w37;
	loc w37: invariant xabs <= 78.08
		when xabs = 78.08 sync E goto w38;
	loc w38: invariant xabs <= 78.28
		when xabs = 78.28 sync G goto w39;
	loc w39: invariant xabs <= 78.4
		when xabs = 78.4 sync C goto w40;
	loc w40: invariant xabs <= 78.52
		when xabs = 78.52 sync B goto w41;
	loc w41: invariant xabs <= 80.84
		when xabs = 80.84 sync A goto w42;
	loc w42: invariant xabs <= 82
		when xabs = 82 sync F goto w43;
	loc w43: invariant xabs <= 83
		when xabs = 83 sync B goto w44;
	loc w44: invariant xabs <= 83.08
		when xabs = 83.08 sync C goto w45;
	loc w45: invariant xabs <= 83.44
		when xabs = 83.44 sync F goto w46;
	loc w46: invariant xabs <= 83.48
		when xabs = 83.48 sync E goto w47;
	loc w47: invariant xabs <= 83.6
		when xabs = 83.6 sync D goto w48;
	loc w48: invariant xabs <= 83.64
		when xabs = 83.64 sync C goto w49;
	loc w49: invariant xabs <= 83.96
		when xabs = 83.96 sync F goto w50;
	loc w50: invariant xabs <= 84.04
		when xabs = 84.04 sync E goto w51;
	loc w51: invariant xabs <= 85.44
		when xabs = 85.44 sync F goto w52;
	loc w52: invariant xabs <= 85.56
		when xabs = 85.56 sync D goto w53;
	loc w53: invariant xabs <= 85.92
		when xabs = 85.92 sync C goto w54;
	loc w54: invariant xabs <= 86.08
		when xabs = 86.08 sync D goto w55;
	loc w55: invariant xabs <= 86.4
		when xabs = 86.4 sync C goto w56;
	loc w56: invariant xabs <= 86.64
		when xabs = 86.64 sync D goto w57;
	loc w57: invariant xabs <= 86.88
		when xabs = 86.88 sync F goto w58;
	loc w58: invariant xabs <= 87.08
		when xabs = 87.08 sync E goto w59;
	loc w59: invariant xabs <= 87.36
		when xabs = 87.36 sync F goto w60;
	loc w60: invariant xabs <= 87.48
		when xabs = 87.48 sync E goto w61;
	loc w61: invariant xabs <= 87.88
		when xabs = 87.88 sync F goto w62;
	loc w62: invariant xabs <= 87.92
		when xabs = 87.92 sync E goto w63;
	loc w63: invariant xabs <= 88.36
		when xabs = 88.36 sync F goto w64;
	loc w64: invariant xabs <= 88.44
		when xabs = 88.44 sync E goto w65;
	loc w65: invariant xabs <= 88.84
		when xabs = 88.84 sync F goto w66;
	loc w66: invariant xabs <= 89.08
		when xabs = 89.08 sync E goto w67;
	loc w67: invariant xabs <= 89.28
		when xabs = 89.28 sync F goto w68;
	loc w68: invariant xabs <= 89.56
		when xabs = 89.56 sync E goto w69;
	loc w69: invariant xabs <= 89.76
		when xabs = 89.76 sync F goto w70;
	loc w70: invariant xabs <= 90
		when xabs = 90 sync E goto w71;
	loc w71: invariant xabs <= 90.28
		when xabs = 90.28 sync F goto w72;
	loc w72: invariant xabs <= 90.52
		when xabs = 90.52 sync E goto w73;
	loc w73: invariant xabs <= 90.8
		when xabs = 90.8 sync F goto w74;
	loc w74: invariant xabs <= 90.88
		when xabs = 90.88 sync E goto w75;
	loc w75: invariant xabs <= 91.28
		when xabs = 91.28 sync F goto w76;
	loc w76: invariant xabs <= 91.4
		when xabs = 91.4 sync E goto w77;
	loc w77: invariant xabs <= 91.76
		when xabs = 91.76 sync F goto w78;
	loc w78: invariant xabs <= 92
		when xabs = 92 sync E goto w79;
	loc w79: invariant xabs <= 92.24
		when xabs = 92.24 sync F goto w80;
	loc w80: invariant xabs <= 92.52
		when xabs = 92.52 sync E goto w81;
	loc w81: invariant xabs <= 92.72
		when xabs = 92.72 sync F goto w82;
	loc w82: invariant xabs <= 93
		when xabs = 93 sync E goto w83;
	loc w83: invariant xabs <= 93.2
		when xabs = 93.2 sync F goto w84;
	loc w84: invariant xabs <= 93.48
		when xabs = 93.48 sync E goto w85;
	loc w85: invariant xabs <= 93.72
		when xabs = 93.72 sync F goto w86;
	loc w86: invariant xabs <= 93.96
		when xabs = 93.96 sync E goto w87;
	loc w87: invariant xabs <= 94.24
		when xabs = 94.24 sync F goto w88;
	loc w88: invariant xabs <= 94.44
		when xabs = 94.44 sync E goto w89;
	loc w89: invariant xabs <= 94.68
		when xabs = 94.68 sync F goto w90;
	loc w90: invariant xabs <= 94.96
		when xabs = 94.96 sync E goto w91;
	loc w91: invariant xabs <= 95.16
		when xabs = 95.16 sync F goto w92;
	loc w92: invariant xabs <= 95.4
		when xabs = 95.4 sync E goto w93;
	loc w93: invariant xabs <= 95.64
		when xabs = 95.64 sync F goto w94;
	loc w94: invariant xabs <= 95.96
		when xabs = 95.96 sync E goto w95;
	loc w95: invariant xabs <= 96.12
		when xabs = 96.12 sync F goto w96;
	loc w96: invariant xabs <= 96.44
		when xabs = 96.44 sync E goto w97;
	loc w97: invariant xabs <= 96.64
		when xabs = 96.64 sync F goto w98;
	loc w98: invariant xabs <= 96.92
		when xabs = 96.92 sync E goto w99;
	loc w99: invariant xabs <= 97.16
		when xabs = 97.16 sync F goto w100;
	loc w100: invariant xabs <= 97.4
		when xabs = 97.4 sync E goto w101;
	loc w101: invariant xabs <= 97.64
		when xabs = 97.64 sync F goto w102;
	loc w102: invariant xabs <= 97.88
		when xabs = 97.88 sync E goto w103;
	loc w103: invariant xabs <= 98
		when xabs = 98 sync F goto w104;
	loc w104: invariant xabs <= 98.2
		when xabs = 98.2 sync E goto w105;
	loc w105: invariant xabs <= 98.32
		when xabs = 98.32 sync C goto w106;
	loc w106: invariant xabs <= 98.44
		when xabs = 98.44 sync B goto w107;
	loc w107: invariant xabs <= 100.44
		when xabs = 100.44 sync A goto w108;
	loc w108: invariant xabs <= 101.84
		when xabs = 101.84 sync F goto w109;
	loc w109: invariant xabs <= 102.12
		when xabs = 102.12 sync B goto w110;
	loc w110: invariant xabs <= 102.2
		when xabs = 102.2 sync E goto w111;
	loc w111: invariant xabs <= 104.68
		when xabs = 104.68 sync F goto w112;
	loc w112: invariant xabs <= 104.8
		when xabs = 104.8 sync C goto w113;
	loc w113: invariant xabs <= 104.84
		when xabs = 104.84 sync D goto w114;
	loc w114: invariant xabs <= 105.96
		when xabs = 105.96 sync E goto w115;
	loc w115: invariant xabs <= 107.68
		when xabs = 107.68 sync C goto w116;
	loc w116: invariant xabs <= 107.76
		when xabs = 107.76 sync D goto w117;
	loc w117: invariant xabs <= 109.36
		when xabs = 109.36 sync E goto w118;
	loc w118: invariant xabs <= 109.4
		when xabs = 109.4 sync F goto w119;
	loc w119: invariant xabs <= 110.56
		when xabs = 110.56 sync C goto w120;
	loc w120: invariant xabs <= 110.68
		when xabs = 110.68 sync D goto w121;
	loc w121: invariant xabs <= 112.72
		when xabs = 112.72 sync E goto w122;
	loc w122: invariant xabs <= 112.88
		when xabs = 112.88 sync F goto w123;
	loc w123: invariant xabs <= 113.48
		when xabs = 113.48 sync C goto w124;
	loc w124: invariant xabs <= 113.56
		when xabs = 113.56 sync D goto w125;
	loc w125: invariant xabs <= 118.16
		when xabs = 118.16 sync E goto w126;
	loc w126: invariant xabs <= 118.28
		when xabs = 118.28 sync C goto w127;
	loc w127: invariant xabs <= 118.44
		when xabs = 118.44 sync B goto w128;
	loc w128: invariant xabs <= 122.6
		when xabs = 122.6 sync A goto w129;
	loc w129: invariant xabs <= 122.84
		when xabs = 122.84 sync B goto w130;
	loc w130: invariant xabs <= 123.08
		when xabs = 123.08 sync A goto w131;
	loc w131: invariant xabs <= 123.36
		when xabs = 123.36 sync B goto w132;
	loc w132: invariant xabs <= 123.52
		when xabs = 123.52 sync A goto w133;
	loc w133: invariant xabs <= 123.88
		when xabs = 123.88 sync B goto w134;
	loc w134: invariant xabs <= 124
		when xabs = 124 sync A goto w135;
	loc w135: invariant xabs <= 124.36
		when xabs = 124.36 sync B goto w136;
	loc w136: invariant xabs <= 124.52
		when xabs = 124.52 sync A goto w137;
	loc w137: invariant xabs <= 124.84
		when xabs = 124.84 sync B goto w138;
	loc w138: invariant xabs <= 125
		when xabs = 125 sync A goto w139;
	loc w139: invariant xabs <= 125.32
		when xabs = 125.32 sync B goto w140;
	loc w140: invariant xabs <= 125.52
		when xabs = 125.52 sync A goto w141;
	loc w141: invariant xabs <= 125.8
		when xabs = 125.8 sync B goto w142;
	loc w142: invariant xabs <= 126
		when xabs = 126 sync A goto w143;
	loc w143: invariant xabs <= 126.32
		when xabs = 126.32 sync B goto w144;
	loc w144: invariant xabs <= 126.48
		when xabs = 126.48 sync A goto w145;
	loc w145: invariant xabs <= 126.8
		when xabs = 126.8 sync B goto w146;
	loc w146: invariant xabs <= 126.96
		when xabs = 126.96 sync A goto w147;
	loc w147: invariant xabs <= 127.32
		when xabs = 127.32 sync B goto w148;
	loc w148: invariant xabs <= 127.44
		when xabs = 127.44 sync A goto w149;
	loc w149: invariant xabs <= 127.8
		when xabs = 127.8 sync B goto w150;
	loc w150: invariant xabs <= 127.96
		when xabs = 127.96 sync A goto w151;
	loc w151: invariant xabs <= 128.24
		when xabs = 128.24 sync B goto w152;
	loc w152: invariant xabs <= 128.44
		when xabs = 128.44 sync A goto w153;
	loc w153: invariant xabs <= 128.72
		when xabs = 128.72 sync B goto w154;
	loc w154: invariant xabs <= 128.84
		when xabs = 128.84 sync A goto w155;
	loc w155: invariant xabs <= 128.88
		when xabs = 128.88 sync F goto w156;
	loc w156: invariant xabs <= 128.92
		when xabs = 128.92 sync E goto w157;
	loc w157: invariant xabs <= 129.24
		when xabs = 129.24 sync B goto w158;
	loc w158: invariant xabs <= 129.4
		when xabs = 129.4 sync A goto w159;
	loc w159: invariant xabs <= 129.76
		when xabs = 129.76 sync B goto w160;
	loc w160: invariant xabs <= 129.88
		when xabs = 129.88 sync A goto w161;
	loc w161: invariant xabs <= 130.24
		when xabs = 130.24 sync B goto w162;
	loc w162: invariant xabs <= 130.36
		when xabs = 130.36 sync A goto w163;
	loc w163: invariant xabs <= 130.72
		when xabs = 130.72 sync B goto w164;
	loc w164: invariant xabs <= 130.88
		when xabs = 130.88 sync A goto w165;
	loc w165: invariant xabs <= 131.2
		when xabs = 131.2 sync B goto w166;
	loc w166: invariant xabs <= 131.36
		when xabs = 131.36 sync A goto w167;
	loc w167: invariant xabs <= 131.68
		when xabs = 131.68 sync B goto w168;
	loc w168: invariant xabs <= 131.88
		when xabs = 131.88 sync A goto w169;
	loc w169: invariant xabs <= 132.16
		when xabs = 132.16 sync B goto w170;
	loc w170: invariant xabs <= 132.36
		when xabs = 132.36 sync A goto w171;
	loc w171: invariant xabs <= 132.68
		when xabs = 132.68 sync B goto w172;
	loc w172: invariant xabs <= 132.84
		when xabs = 132.84 sync A goto w173;
	loc w173: invariant xabs <= 133.68
		when xabs = 133.68 sync B goto w174;
	loc w174: invariant xabs <= 134.32
		when xabs = 134.32 sync A goto w175;
	loc w175: invariant xabs <= 134.64
		when xabs = 134.64 sync B goto w176;
	loc w176: invariant xabs <= 134.8
		when xabs = 134.8 sync A goto w177;
	loc w177: invariant xabs <= 135.12
		when xabs = 135.12 sync B goto w178;
	loc w178: invariant xabs <= 135.32
		when xabs = 135.32 sync A goto w179;
	loc w179: invariant xabs <= 135.6
		when xabs = 135.6 sync B goto w180;
	loc w180: invariant xabs <= 135.8
		when xabs = 135.8 sync A goto w181;
	loc w181: invariant xabs <= 136.12
		when xabs = 136.12 sync B goto w182;
	loc w182: invariant xabs <= 136.28
		when xabs = 136.28 sync A goto w183;
	loc w183: invariant xabs <= 137.56
		when xabs = 137.56 sync B goto w184;
	loc w184: invariant xabs <= 141.68
		when xabs = 141.68 sync A goto w185;
	loc w185: invariant xabs <= 142
		when xabs = 142 sync B goto w186;
	loc w186: invariant xabs <= 142.12
		when xabs = 142.12 sync A goto w187;
	loc w187: invariant xabs <= 142.48
		when xabs = 142.48 sync B goto w188;
	loc w188: invariant xabs <= 142.6
		when xabs = 142.6 sync A goto w189;
	loc w189: invariant xabs <= 143.44
		when xabs = 143.44 sync B goto w190;
	loc w190: invariant xabs <= 144.16
		when xabs = 144.16 sync A goto w191;
	loc w191: invariant xabs <= 144.4
		when xabs = 144.4 sync B goto w192;
	loc w192: invariant xabs <= 148.04
		when xabs = 148.04 sync A goto w193;
	loc w193: invariant xabs <= 148.36
		when xabs = 148.36 sync B goto w194;
	loc w194: invariant xabs <= 148.52
		when xabs = 148.52 sync A goto w195;
	loc w195: invariant xabs <= 148.84
		when xabs = 148.84 sync B goto w196;
	loc w196: invariant xabs <= 149
		when xabs = 149 sync A goto w197;
	loc w197: invariant xabs <= 149.36
		when xabs = 149.36 sync B goto w198;
	loc w198: invariant xabs <= 149.48
		when xabs = 149.48 sync A goto w199;
	loc w199: invariant xabs <= 149.84
		when xabs = 149.84 sync B goto w200;
	loc w200: invariant xabs <= 149.96
		when xabs = 149.96 sync A goto w201;
	loc w201: invariant xabs <= 150.32
		when xabs = 150.32 sync B goto w202;
	loc w202: invariant xabs <= 150.48
		when xabs = 150.48 sync A goto w203;
	loc w203: invariant xabs <= 150.8
		when xabs = 150.8 sync B goto w204;
	loc w204: invariant xabs <= 150.96
		when xabs = 150.96 sync A goto w205;
	loc w205: invariant xabs <= 151.28
		when xabs = 151.28 sync B goto w206;
	loc w206: invariant xabs <= 151.44
		when xabs = 151.44 sync A goto w207;
	loc w207: invariant xabs <= 151.8
		when xabs = 151.8 sync B goto w208;
	loc w208: invariant xabs <= 153.92
		when xabs = 153.92 sync A goto w209;
	loc w209: invariant xabs <= 154.2
		when xabs = 154.2 sync B goto w210;
	loc w210: invariant xabs <= 154.4
		when xabs = 154.4 sync A goto w211;
	loc w211: invariant xabs <= 154.72
		when xabs = 154.72 sync B goto w212;
	loc w212: invariant xabs <= 154.88
		when xabs = 154.88 sync A goto w213;
	loc w213: invariant xabs <= 155.2
		when xabs = 155.2 sync B goto w214;
	loc w214: invariant xabs <= 155.36
		when xabs = 155.36 sync A goto w215;
	loc w215: invariant xabs <= 155.72
		when xabs = 155.72 sync B goto w216;
	loc w216: invariant xabs <= 155.84
		when xabs = 155.84 sync A goto w217;
	loc w217: invariant xabs <= 156.2
		when xabs = 156.2 sync B goto w218;
	loc w218: invariant xabs <= 156.36
		when xabs = 156.36 sync A goto w219;
	loc w219: invariant xabs <= 156.64
		when xabs = 156.64 sync B goto w220;
	loc w220: invariant xabs <= 156.84
		when xabs = 156.84 sync A goto w221;
	loc w221: invariant xabs <= 157.12
		when xabs = 157.12 sync B goto w222;
	loc w222: invariant xabs <= 157.36
		when xabs = 157.36 sync A goto w223;
	loc w223: invariant xabs <= 157.64
		when xabs = 157.64 sync B goto w224;
	loc w224: invariant xabs <= 157.84
		when xabs = 157.84 sync A goto w225;
	loc w225: invariant xabs <= 158.24
		when xabs = 158.24 sync B goto w226;
	loc w226: invariant xabs <= 161.24
		when xabs = 161.24 sync A goto w227;
	loc w227: invariant xabs <= 161.56
		when xabs = 161.56 sync B goto w228;
	loc w228: invariant xabs <= 161.72
		when xabs = 161.72 sync A goto w229;
	loc w229: invariant xabs <= 162.04
		when xabs = 162.04 sync B goto w230;
	loc w230: invariant xabs <= 162.2
		when xabs = 162.2 sync A goto w231;
	loc w231: invariant xabs <= 162.52
		when xabs = 162.52 sync B goto w232;
	loc w232: invariant xabs <= 162.72
		when xabs = 162.72 sync A goto w233;
	loc w233: invariant xabs <= 163
		when xabs = 163 sync B goto w234;
	loc w234: invariant xabs <= 163.24
		when xabs = 163.24 sync A goto w235;
	loc w235: invariant xabs <= 163.48
		when xabs = 163.48 sync B goto w236;
	loc w236: invariant xabs <= 163.72
		when xabs = 163.72 sync A goto w237;
	loc w237: invariant xabs <= 164
		when xabs = 164 sync B goto w238;
	loc w238: invariant xabs <= 164.2
		when xabs = 164.2 sync A goto w239;
	loc w239: invariant xabs <= 164.48
		when xabs = 164.48 sync B goto w240;
	loc w240: invariant xabs <= 164.68
		when xabs = 164.68 sync A goto w241;
	loc w241: invariant xabs <= 165
		when xabs = 165 sync B goto w242;
	loc w242: invariant xabs <= 165.16
		when xabs = 165.16 sync A goto w243;
	loc w243: invariant xabs <= 165.48
		when xabs = 165.48 sync B goto w244;
	loc w244: invariant xabs <= 165.68
		when xabs = 165.68 sync A goto w245;
	loc w245: invariant xabs <= 165.96
		when xabs = 165.96 sync B goto w246;
	loc w246: invariant xabs <= 166.16
		when xabs = 166.16 sync A goto w247;
	loc w247: invariant xabs <= 166.44
		when xabs = 166.44 sync B goto w248;
	loc w248: invariant xabs <= 166.56
		when xabs = 166.56 sync A goto w249;
	loc w249: invariant xabs <= 166.6
		when xabs = 166.6 sync F goto w250;
	loc w250: invariant xabs <= 166.68
		when xabs = 166.68 sync E goto w251;
	loc w251: invariant xabs <= 166.92
		when xabs = 166.92 sync B goto w252;
	loc w252: invariant xabs <= 167
		when xabs = 167 sync A goto w253;
	loc w253: invariant xabs <= 167.08
		when xabs = 167.08 sync F goto w254;
	loc w254: invariant xabs <= 167.16
		when xabs = 167.16 sync E goto w255;
	loc w255: invariant xabs <= 167.44
		when xabs = 167.44 sync B goto w256;
	loc w256: invariant xabs <= 167.52
		when xabs = 167.52 sync A goto w257;
	loc w257: invariant xabs <= 167.56
		when xabs = 167.56 sync F goto w258;
	loc w258: invariant xabs <= 167.6
		when xabs = 167.6 sync E goto w259;
	loc w259: invariant xabs <= 167.92
		when xabs = 167.92 sync B goto w260;
	loc w260: invariant xabs <= 168
		when xabs = 168 sync A goto w261;
	loc w261: invariant xabs <= 168.04
		when xabs = 168.04 sync F goto w262;
	loc w262: invariant xabs <= 168.12
		when xabs = 168.12 sync E goto w263;
	loc w263: invariant xabs <= 168.4
		when xabs = 168.4 sync B goto w264;
	loc w264: invariant xabs <= 168.48
		when xabs = 168.48 sync A goto w265;
	loc w265: invariant xabs <= 168.52
		when xabs = 168.52 sync F goto w266;
	loc w266: invariant xabs <= 168.6
		when xabs = 168.6 sync E goto w267;
	loc w267: invariant xabs <= 168.88
		when xabs = 168.88 sync B goto w268;
	loc w268: invariant xabs <= 168.96
		when xabs = 168.96 sync A goto w269;
	loc w269: invariant xabs <= 169.04
		when xabs = 169.04 sync F goto w270;
	loc w270: invariant xabs <= 169.12
		when xabs = 169.12 sync E goto w271;
	loc w271: invariant xabs <= 169.36
		when xabs = 169.36 sync B goto w272;
	loc w272: invariant xabs <= 169.44
		when xabs = 169.44 sync A goto w273;
	loc w273: invariant xabs <= 169.56
		when xabs = 169.56 sync F goto w274;
	loc w274: invariant xabs <= 169.6
		when xabs = 169.6 sync E goto w275;
	loc w275: invariant xabs <= 169.84
		when xabs = 169.84 sync B goto w276;
	loc w276: invariant xabs <= 169.92
		when xabs = 169.92 sync A goto w277;
	loc w277: invariant xabs <= 170.04
		when xabs = 170.04 sync F goto w278;
	loc w278: invariant xabs <= 170.08
		when xabs = 170.08 sync E goto w279;
	loc w279: invariant xabs <= 170.36
		when xabs = 170.36 sync B goto w280;
	loc w280: invariant xabs <= 170.4
		when xabs = 170.4 sync A goto w281;
	loc w281: invariant xabs <= 170.52
		when xabs = 170.52 sync F goto w282;
	loc w282: invariant xabs <= 170.56
		when xabs = 170.56 sync E goto w283;
	loc w283: invariant xabs <= 170.84
		when xabs = 170.84 sync B goto w284;
	loc w284: invariant xabs <= 170.92
		when xabs = 170.92 sync A goto w285;
	loc w285: invariant xabs <= 171
		when xabs = 171 sync F goto w286;
	loc w286: invariant xabs <= 171.04
		when xabs = 171.04 sync E goto w287;
	loc w287: invariant xabs <= 171.36
		when xabs = 171.36 sync B goto w288;
	loc w288: invariant xabs <= 171.4
		when xabs = 171.4 sync A goto w289;
	loc w289: invariant xabs <= 171.52
		when xabs = 171.52 sync F goto w290;
	loc w290: invariant xabs <= 171.84
		when xabs = 171.84 sync B goto w291;
	loc w291: invariant xabs <= 171.88
		when xabs = 171.88 sync A goto w292;
	loc w292: invariant xabs <= 172
		when xabs = 172 sync F goto w293;
	loc w293: invariant xabs <= 172.04
		when xabs = 172.04 sync E goto w294;
	loc w294: invariant xabs <= 172.32
		when xabs = 172.32 sync B goto w295;
	loc w295: invariant xabs <= 172.36
		when xabs = 172.36 sync A goto w296;
	loc w296: invariant xabs <= 172.52
		when xabs = 172.52 sync F goto w297;
	loc w297: invariant xabs <= 172.56
		when xabs = 172.56 sync E goto w298;
	loc w298: invariant xabs <= 172.84
		when xabs = 172.84 sync B goto w299;
	loc w299: invariant xabs <= 173
		when xabs = 173 sync F goto w300;
	loc w300: invariant xabs <= 173.04
		when xabs = 173.04 sync E goto w301;
	loc w301: invariant xabs <= 173.28
		when xabs = 173.28 sync C goto w302;
	loc w302: invariant xabs <= 173.36
		when xabs = 173.36 sync B goto w303;
	loc w303: invariant xabs <= 173.48
		when xabs = 173.48 sync F goto w304;
	loc w304: invariant xabs <= 173.52
		when xabs = 173.52 sync E goto w305;
	loc w305: invariant xabs <= 173.76
		when xabs = 173.76 sync C goto w306;
	loc w306: invariant xabs <= 173.84
		when xabs = 173.84 sync B goto w307;
	loc w307: invariant xabs <= 173.96
		when xabs = 173.96 sync F goto w308;
	loc w308: invariant xabs <= 174
		when xabs = 174 sync E goto w309;
	loc w309: invariant xabs <= 174.28
		when xabs = 174.28 sync C goto w310;
	loc w310: invariant xabs <= 174.32
		when xabs = 174.32 sync B goto w311;
	loc w311: invariant xabs <= 174.44
		when xabs = 174.44 sync F goto w312;
	loc w312: invariant xabs <= 174.48
		when xabs = 174.48 sync E goto w313;
	loc w313: invariant xabs <= 174.76
		when xabs = 174.76 sync C goto w314;
	loc w314: invariant xabs <= 174.8
		when xabs = 174.8 sync B goto w315;
	loc w315: invariant xabs <= 174.92
		when xabs = 174.92 sync F goto w316;
	loc w316: invariant xabs <= 175
		when xabs = 175 sync E goto w317;
	loc w317: invariant xabs <= 175.24
		when xabs = 175.24 sync C goto w318;
	loc w318: invariant xabs <= 175.32
		when xabs = 175.32 sync B goto w319;
	loc w319: invariant xabs <= 175.44
		when xabs = 175.44 sync F goto w320;
	loc w320: invariant xabs <= 175.48
		when xabs = 175.48 sync E goto w321;
	loc w321: invariant xabs <= 175.72
		when xabs = 175.72 sync C goto w322;
	loc w322: invariant xabs <= 175.76
		when xabs = 175.76 sync B goto w323;
	loc w323: invariant xabs <= 175.96
		when xabs = 175.96 sync F goto w324;
	loc w324: invariant xabs <= 176
		when xabs = 176 sync E goto w325;
	loc w325: invariant xabs <= 176.2
		when xabs = 176.2 sync C goto w326;
	loc w326: invariant xabs <= 176.24
		when xabs = 176.24 sync B goto w327;
	loc w327: invariant xabs <= 176.44
		when xabs = 176.44 sync F goto w328;
	loc w328: invariant xabs <= 176.48
		when xabs = 176.48 sync E goto w329;
	loc w329: invariant xabs <= 176.68
		when xabs = 176.68 sync C goto w330;
	loc w330: invariant xabs <= 176.76
		when xabs = 176.76 sync B goto w331;
	loc w331: invariant xabs <= 176.88
		when xabs = 176.88 sync F goto w332;
	loc w332: invariant xabs <= 176.96
		when xabs = 176.96 sync E goto w333;
	loc w333: invariant xabs <= 177.2
		when xabs = 177.2 sync C goto w334;
	loc w334: invariant xabs <= 177.28
		when xabs = 177.28 sync B goto w335;
	loc w335: invariant xabs <= 177.36
		when xabs = 177.36 sync F goto w336;
	loc w336: invariant xabs <= 177.44
		when xabs = 177.44 sync E goto w337;
	loc w337: invariant xabs <= 177.68
		when xabs = 177.68 sync C goto w338;
	loc w338: invariant xabs <= 177.76
		when xabs = 177.76 sync B goto w339;
	loc w339: invariant xabs <= 177.88
		when xabs = 177.88 sync F goto w340;
	loc w340: invariant xabs <= 177.92
		when xabs = 177.92 sync E goto w341;
	loc w341: invariant xabs <= 178.12
		when xabs = 178.12 sync C goto w342;
	loc w342: invariant xabs <= 178.24
		when xabs = 178.24 sync B goto w343;
	loc w343: invariant xabs <= 181.36
		when xabs = 181.36 sync A goto w344;
	loc w344: invariant xabs <= 181.6
		when xabs = 181.6 sync B goto w345;
	loc w345: invariant xabs <= 181.88
		when xabs = 181.88 sync A goto w346;
	loc w346: invariant xabs <= 182.08
		when xabs = 182.08 sync B goto w347;
	loc w347: invariant xabs <= 182.24
		when xabs = 182.24 sync A goto w348;
	loc w348: invariant xabs <= 182.28
		when xabs = 182.28 sync F goto w349;
	loc w349: invariant xabs <= 182.36
		when xabs = 182.36 sync E goto w350;
	loc w350: invariant xabs <= 182.56
		when xabs = 182.56 sync B goto w351;
	loc w351: invariant xabs <= 182.72
		when xabs = 182.72 sync A goto w352;
	loc w352: invariant xabs <= 182.8
		when xabs = 182.8 sync F goto w353;
	loc w353: invariant xabs <= 182.84
		when xabs = 182.84 sync E goto w354;
	loc w354: invariant xabs <= 183.04
		when xabs = 183.04 sync B goto w355;
	loc w355: invariant xabs <= 183.16
		when xabs = 183.16 sync A goto w356;
	loc w356: invariant xabs <= 183.28
		when xabs = 183.28 sync F goto w357;
	loc w357: invariant xabs <= 183.32
		when xabs = 183.32 sync E goto w358;
	loc w358: invariant xabs <= 183.56
		when xabs = 183.56 sync B goto w359;
	loc w359: invariant xabs <= 183.64
		when xabs = 183.64 sync A goto w360;
	loc w360: invariant xabs <= 183.76
		when xabs = 183.76 sync F goto w361;
	loc w361: invariant xabs <= 183.8
		when xabs = 183.8 sync E goto w362;
	loc w362: invariant xabs <= 184.04
		when xabs = 184.04 sync B goto w363;
	loc w363: invariant xabs <= 184.12
		when xabs = 184.12 sync A goto w364;
	loc w364: invariant xabs <= 184.28
		when xabs = 184.28 sync F goto w365;
	loc w365: invariant xabs <= 184.32
		when xabs = 184.32 sync E goto w366;
	loc w366: invariant xabs <= 184.52
		when xabs = 184.52 sync B goto w367;
	loc w367: invariant xabs <= 184.56
		when xabs = 184.56 sync A goto w368;
	loc w368: invariant xabs <= 184.8
		when xabs = 184.8 sync F goto w369;
	loc w369: invariant xabs <= 185
		when xabs = 185 sync B goto w370;
	loc w370: invariant xabs <= 185.04
		when xabs = 185.04 sync A goto w371;
	loc w371: invariant xabs <= 185.32
		when xabs = 185.32 sync F goto w372;
	loc w372: invariant xabs <= 185.52
		when xabs = 185.52 sync B goto w373;
	loc w373: invariant xabs <= 185.76
		when xabs = 185.76 sync F goto w374;
	loc w374: invariant xabs <= 185.8
		when xabs = 185.8 sync E goto w375;
	loc w375: invariant xabs <= 185.96
		when xabs = 185.96 sync C goto w376;
	loc w376: invariant xabs <= 186.04
		when xabs = 186.04 sync B goto w377;
	loc w377: invariant xabs <= 186.24
		when xabs = 186.24 sync F goto w378;
	loc w378: invariant xabs <= 186.28
		when xabs = 186.28 sync E goto w379;
	loc w379: invariant xabs <= 186.48
		when xabs = 186.48 sync C goto w380;
	loc w380: invariant xabs <= 186.52
		when xabs = 186.52 sync B goto w381;
	loc w381: invariant xabs <= 186.72
		when xabs = 186.72 sync F goto w382;
	loc w382: invariant xabs <= 186.76
		when xabs = 186.76 sync E goto w383;
	loc w383: invariant xabs <= 186.96
		when xabs = 186.96 sync C goto w384;
	loc w384: invariant xabs <= 187.04
		when xabs = 187.04 sync B goto w385;
	loc w385: invariant xabs <= 187.2
		when xabs = 187.2 sync F goto w386;
	loc w386: invariant xabs <= 187.24
		when xabs = 187.24 sync E goto w387;
	loc w387: invariant xabs <= 187.44
		when xabs = 187.44 sync C goto w388;
	loc w388: invariant xabs <= 187.52
		when xabs = 187.52 sync B goto w389;
	loc w389: invariant xabs <= 187.72
		when xabs = 187.72 sync F goto w390;
	loc w390: invariant xabs <= 187.76
		when xabs = 187.76 sync E goto w391;
	loc w391: invariant xabs <= 187.92
		when xabs = 187.92 sync C goto w392;
	loc w392: invariant xabs <= 187.96
		when xabs = 187.96 sync B goto w393;
	loc w393: invariant xabs <= 188.24
		when xabs = 188.24 sync F goto w394;
	loc w394: invariant xabs <= 188.4
		when xabs = 188.4 sync C goto w395;
	loc w395: invariant xabs <= 188.44
		when xabs = 188.44 sync B goto w396;
	loc w396: invariant xabs <= 188.76
		when xabs = 188.76 sync F goto w397;
	loc w397: invariant xabs <= 188.88
		when xabs = 188.88 sync C goto w398;
	loc w398: invariant xabs <= 188.92
		when xabs = 188.92 sync B goto w399;
	loc w399: invariant xabs <= 189.2
		when xabs = 189.2 sync F goto w400;
	loc w400: invariant xabs <= 189.24
		when xabs = 189.24 sync E goto w401;
	loc w401: invariant xabs <= 189.44
		when xabs = 189.44 sync C goto w402;
	loc w402: invariant xabs <= 189.68
		when xabs = 189.68 sync B goto w403;
	loc w403: invariant xabs <= 189.72
		when xabs = 189.72 sync E goto w404;
	loc w404: invariant xabs <= 189.96
		when xabs = 189.96 sync C goto w405;
	loc w405: invariant xabs <= 190.16
		when xabs = 190.16 sync F goto w406;
	loc w406: invariant xabs <= 190.2
		when xabs = 190.2 sync E goto w407;
	loc w407: invariant xabs <= 190.4
		when xabs = 190.4 sync D goto w408;
	loc w408: invariant xabs <= 190.48
		when xabs = 190.48 sync C goto w409;
	loc w409: invariant xabs <= 190.64
		when xabs = 190.64 sync F goto w410;
	loc w410: invariant xabs <= 190.72
		when xabs = 190.72 sync E goto w411;
	loc w411: invariant xabs <= 190.88
		when xabs = 190.88 sync D goto w412;
	loc w412: invariant xabs <= 190.92
		when xabs = 190.92 sync C goto w413;
	loc w413: invariant xabs <= 191.16
		when xabs = 191.16 sync F goto w414;
	loc w414: invariant xabs <= 191.2
		when xabs = 191.2 sync E goto w415;
	loc w415: invariant xabs <= 191.32
		when xabs = 191.32 sync D goto w416;
	loc w416: invariant xabs <= 191.36
		when xabs = 191.36 sync C goto w417;
	loc w417: invariant xabs <= 191.68
		when xabs = 191.68 sync F goto w418;
	loc w418: invariant xabs <= 191.76
		when xabs = 191.76 sync E goto w419;
	loc w419: invariant xabs <= 192.16
		when xabs = 192.16 sync F goto w420;
	loc w420: invariant xabs <= 192.2
		when xabs = 192.2 sync E goto w421;
	loc w421: invariant xabs <= 192.32
		when xabs = 192.32 sync D goto w422;
	loc w422: invariant xabs <= 192.36
		when xabs = 192.36 sync C goto w423;
	loc w423: invariant xabs <= 192.64
		when xabs = 192.64 sync F goto w424;
	loc w424: invariant xabs <= 192.84
		when xabs = 192.84 sync D goto w425;
	loc w425: invariant xabs <= 192.88
		when xabs = 192.88 sync C goto w426;
	loc w426: invariant xabs <= 193.12
		when xabs = 193.12 sync F goto w427;
	loc w427: invariant xabs <= 193.32
		when xabs = 193.32 sync D goto w428;
	loc w428: invariant xabs <= 193.36
		when xabs = 193.36 sync C goto w429;
	loc w429: invariant xabs <= 193.6
		when xabs = 193.6 sync F goto w430;
	loc w430: invariant xabs <= 193.64
		when xabs = 193.64 sync E goto w431;
	loc w431: invariant xabs <= 193.8
		when xabs = 193.8 sync D goto w432;
	loc w432: invariant xabs <= 193.84
		when xabs = 193.84 sync C goto w433;
	loc w433: invariant xabs <= 194.12
		when xabs = 194.12 sync F goto w434;
	loc w434: invariant xabs <= 194.24
		when xabs = 194.24 sync D goto w435;
	loc w435: invariant xabs <= 194.28
		when xabs = 194.28 sync F goto w436;
	loc w436: invariant xabs <= 195.12
		when xabs = 195.12 sync C goto w437;
	loc w437: invariant xabs <= 195.24
		when xabs = 195.24 sync D goto w438;
	loc w438: invariant xabs <= 195.6
		when xabs = 195.6 sync C goto w439;
	loc w439: invariant xabs <= 195.72
		when xabs = 195.72 sync D goto w440;
	loc w440: invariant xabs <= 195.76
		when xabs = 195.76 sync F goto w441;
	loc w441: invariant xabs <= 196.08
		when xabs = 196.08 sync C goto w442;
	loc w442: invariant xabs <= 196.24
		when xabs = 196.24 sync D goto w443;
	loc w443: invariant xabs <= 196.28
		when xabs = 196.28 sync C goto w444;
	loc w444: invariant xabs <= 196.56
		when xabs = 196.56 sync F goto w445;
	loc w445: invariant xabs <= 196.72
		when xabs = 196.72 sync D goto w446;
	loc w446: invariant xabs <= 196.8
		when xabs = 196.8 sync C goto w447;
	loc w447: invariant xabs <= 197.08
		when xabs = 197.08 sync F goto w448;
	loc w448: invariant xabs <= 197.12
		when xabs = 197.12 sync D goto w449;
	loc w449: invariant xabs <= 197.2
		when xabs = 197.2 sync F goto w450;
	loc w450: invariant xabs <= 198
		when xabs = 198 sync C goto w451;
	loc w451: invariant xabs <= 198.24
		when xabs = 198.24 sync E goto w452;
	loc w452: invariant xabs <= 198.36
		when xabs = 198.36 sync B goto w453;
	loc w453: invariant xabs <= 200.4
		when xabs = 200.4 sync A goto w454;
	loc w454: invariant xabs <= 201.68
		when xabs = 201.68 sync F goto w455;
	loc w455: invariant xabs <= 203.96
		when xabs = 203.96 sync B goto w456;
	loc w456: invariant xabs <= 207.6
		when xabs = 207.6 sync C goto w457;
	loc w457: invariant xabs <= 207.68
		when xabs = 207.68 sync H goto w458;
	loc w458: invariant xabs <= 218
		when xabs = 218 sync D goto w459;
	loc w459: invariant xabs <= 218.12
		when xabs = 218.12 sync E goto w460;
	loc w460: invariant xabs <= 218.32
		when xabs = 218.32 sync G goto w461;
	loc w461: invariant xabs <= 218.44
		when xabs = 218.44 sync C goto w462;
	loc w462: invariant xabs <= 218.56
		when xabs = 218.56 sync B goto w463;
	loc w463: invariant xabs <= 220.36
		when xabs = 220.36 sync A goto w464;
	loc w464: invariant xabs <= 221.36
		when xabs = 221.36 sync F goto w465;
	loc w465: invariant xabs <= 222.88
		when xabs = 222.88 sync B goto w466;
	loc w466: invariant xabs <= 225.28
		when xabs = 225.28 sync C goto w467;
	loc w467: invariant xabs <= 225.36
		when xabs = 225.36 sync H goto w468;
	loc w468: invariant xabs <= 238
		when xabs = 238 sync D goto w469;
	loc w469: invariant xabs <= 238.12
		when xabs = 238.12 sync E goto w470;
	loc w470: invariant xabs <= 238.32
		when xabs = 238.32 sync G goto w471;
	loc w471: invariant xabs <= 238.44
		when xabs = 238.44 sync C goto w472;
	loc w472: invariant xabs <= 238.56
		when xabs = 238.56 sync B goto w473;
	loc w473: invariant xabs <= 240.36
		when xabs = 240.36 sync A goto w474;
	loc w474: invariant xabs <= 241.2
		when xabs = 241.2 sync F goto w475;
	loc w475: invariant xabs <= 242.4
		when xabs = 242.4 sync B goto w476;
	loc w476: invariant xabs <= 245.24
		when xabs = 245.24 sync C goto w477;
	loc w477: invariant xabs <= 245.32
		when xabs = 245.32 sync H goto w478;
	loc w478: invariant xabs <= 258
		when xabs = 258 sync D goto w479;
	loc w479: invariant xabs <= 258.12
		when xabs = 258.12 sync E goto w480;
	loc w480: invariant xabs <= 258.32
		when xabs = 258.32 sync G goto w481;
	loc w481: invariant xabs <= 258.44
		when xabs = 258.44 sync C goto w482;
	loc w482: invariant xabs <= 258.56
		when xabs = 258.56 sync B goto w483;
	loc w483: invariant xabs <= 260.36
		when xabs = 260.36 sync A goto w484;
	loc w484: invariant xabs <= 261.2
		when xabs = 261.2 sync F goto w485;
	loc w485: invariant xabs <= 263.44
		when xabs = 263.44 sync B goto w486;
	loc w486: invariant xabs <= 265.16
		when xabs = 265.16 sync C goto w487;
	loc w487: invariant xabs <= 267.36
		when xabs = 267.36 sync D goto w488;
	loc w488: invariant xabs <= 268.56
		when xabs = 268.56 sync H goto w489;
	loc w489: invariant xabs <= 268.64
		when xabs = 268.64 sync E goto w490;
	loc w490: invariant xabs <= 271.48
		when xabs = 271.48 sync F goto w491;
	loc w491: invariant xabs <= 271.6
		when xabs = 271.6 sync E goto w492;
	loc w492: invariant xabs <= 272
		when xabs = 272 sync F goto w493;
	loc w493: invariant xabs <= 272.12
		when xabs = 272.12 sync E goto w494;
	loc w494: invariant xabs <= 274.44
		when xabs = 274.44 sync F goto w495;
	loc w495: invariant xabs <= 274.6
		when xabs = 274.6 sync E goto w496;
	loc w496: invariant xabs <= 274.92
		when xabs = 274.92 sync F goto w497;
	loc w497: invariant xabs <= 275.16
		when xabs = 275.16 sync E goto w498;
	loc w498: invariant xabs <= 275.4
		when xabs = 275.4 sync F goto w499;
	loc w499: invariant xabs <= 275.56
		when xabs = 275.56 sync E goto w500;
	loc w500: invariant xabs <= 277.36
		when xabs = 277.36 sync F goto w501;
	loc w501: invariant xabs <= 277.56
		when xabs = 277.56 sync E goto w502;
	loc w502: invariant xabs <= 277.84
		when xabs = 277.84 sync F goto w503;
	loc w503: invariant xabs <= 278.04
		when xabs = 278.04 sync E goto w504;
	loc w504: invariant xabs <= 278.24
		when xabs = 278.24 sync G goto w505;
	loc w505: invariant xabs <= 278.36
		when xabs = 278.36 sync C goto w506;
	loc w506: invariant xabs <= 278.48
		when xabs = 278.48 sync B goto w507;
	loc w507: invariant xabs <= 281.28
		when xabs = 281.28 sync A goto w508;
	loc w508: invariant xabs <= 281.48
		when xabs = 281.48 sync B goto w509;
	loc w509: invariant xabs <= 281.76
		when xabs = 281.76 sync A goto w510;
	loc w510: invariant xabs <= 281.96
		when xabs = 281.96 sync B goto w511;
	loc w511: invariant xabs <= 282.04
		when xabs = 282.04 sync A goto w512;
	loc w512: invariant xabs <= 282.24
		when xabs = 282.24 sync F goto w513;
	loc w513: invariant xabs <= 282.28
		when xabs = 282.28 sync E goto w514;
	loc w514: invariant xabs <= 282.4
		when xabs = 282.4 sync B goto w515;
	loc w515: invariant xabs <= 282.48
		when xabs = 282.48 sync A goto w516;
	loc w516: invariant xabs <= 282.76
		when xabs = 282.76 sync F goto w517;
	loc w517: invariant xabs <= 282.92
		when xabs = 282.92 sync B goto w518;
	loc w518: invariant xabs <= 282.96
		when xabs = 282.96 sync A goto w519;
	loc w519: invariant xabs <= 283.24
		when xabs = 283.24 sync F goto w520;
	loc w520: invariant xabs <= 283.4
		when xabs = 283.4 sync B goto w521;
	loc w521: invariant xabs <= 283.48
		when xabs = 283.48 sync A goto w522;
	loc w522: invariant xabs <= 283.68
		when xabs = 283.68 sync F goto w523;
	loc w523: invariant xabs <= 283.72
		when xabs = 283.72 sync E goto w524;
	loc w524: invariant xabs <= 283.92
		when xabs = 283.92 sync B goto w525;
	loc w525: invariant xabs <= 283.96
		when xabs = 283.96 sync A goto w526;
	loc w526: invariant xabs <= 284.16
		when xabs = 284.16 sync F goto w527;
	loc w527: invariant xabs <= 284.2
		when xabs = 284.2 sync E goto w528;
	loc w528: invariant xabs <= 284.48
		when xabs = 284.48 sync B goto w529;
	loc w529: invariant xabs <= 284.64
		when xabs = 284.64 sync F goto w530;
	loc w530: invariant xabs <= 284.68
		when xabs = 284.68 sync E goto w531;
	loc w531: invariant xabs <= 284.88
		when xabs = 284.88 sync C goto w532;
	loc w532: invariant xabs <= 284.96
		when xabs = 284.96 sync B goto w533;
	loc w533: invariant xabs <= 285.16
		when xabs = 285.16 sync F goto w534;
	loc w534: invariant xabs <= 285.2
		when xabs = 285.2 sync E goto w535;
	loc w535: invariant xabs <= 285.36
		when xabs = 285.36 sync C goto w536;
	loc w536: invariant xabs <= 285.44
		when xabs = 285.44 sync B goto w537;
	loc w537: invariant xabs <= 285.64
		when xabs = 285.64 sync F goto w538;
	loc w538: invariant xabs <= 285.72
		when xabs = 285.72 sync E goto w539;
	loc w539: invariant xabs <= 285.88
		when xabs = 285.88 sync C goto w540;
	loc w540: invariant xabs <= 285.92
		when xabs = 285.92 sync B goto w541;
	loc w541: invariant xabs <= 286.16
		when xabs = 286.16 sync F goto w542;
	loc w542: invariant xabs <= 286.2
		when xabs = 286.2 sync E goto w543;
	loc w543: invariant xabs <= 286.36
		when xabs = 286.36 sync C goto w544;
	loc w544: invariant xabs <= 286.4
		when xabs = 286.4 sync B goto w545;
	loc w545: invariant xabs <= 286.64
		when xabs = 286.64 sync F goto w546;
	loc w546: invariant xabs <= 286.88
		when xabs = 286.88 sync C goto w547;
	loc w547: invariant xabs <= 286.92
		when xabs = 286.92 sync B goto w548;
	loc w548: invariant xabs <= 287.08
		when xabs = 287.08 sync F goto w549;
	loc w549: invariant xabs <= 287.12
		when xabs = 287.12 sync E goto w550;
	loc w550: invariant xabs <= 287.36
		when xabs = 287.36 sync C goto w551;
	loc w551: invariant xabs <= 287.4
		when xabs = 287.4 sync B goto w552;
	loc w552: invariant xabs <= 287.6
		when xabs = 287.6 sync F goto w553;
	loc w553: invariant xabs <= 287.84
		when xabs = 287.84 sync C goto w554;
	loc w554: invariant xabs <= 287.92
		when xabs = 287.92 sync B goto w555;
	loc w555: invariant xabs <= 288.08
		when xabs = 288.08 sync F goto w556;
	loc w556: invariant xabs <= 288.12
		when xabs = 288.12 sync E goto w557;
	loc w557: invariant xabs <= 288.36
		when xabs = 288.36 sync C goto w558;
	loc w558: invariant xabs <= 288.56
		when xabs = 288.56 sync F goto w559;
	loc w559: invariant xabs <= 288.64
		when xabs = 288.64 sync E goto w560;
	loc w560: invariant xabs <= 288.8
		when xabs = 288.8 sync D goto w561;
	loc w561: invariant xabs <= 288.88
		when xabs = 288.88 sync C goto w562;
	loc w562: invariant xabs <= 288.92
		when xabs = 288.92 sync F goto w563;
	loc w563: invariant xabs <= 289.08
		when xabs = 289.08 sync B goto w564;
	loc w564: invariant xabs <= 289.12
		when xabs = 289.12 sync E goto w565;
	loc w565: invariant xabs <= 289.28
		when xabs = 289.28 sync C goto w566;
	loc w566: invariant xabs <= 289.36
		when xabs = 289.36 sync B goto w567;
	loc w567: invariant xabs <= 289.56
		when xabs = 289.56 sync F goto w568;
	loc w568: invariant xabs <= 289.6
		when xabs = 289.6 sync E goto w569;
	loc w569: invariant xabs <= 289.84
		when xabs = 289.84 sync C goto w570;
	loc w570: invariant xabs <= 290.04
		when xabs = 290.04 sync F goto w571;
	loc w571: invariant xabs <= 290.08
		when xabs = 290.08 sync E goto w572;
	loc w572: invariant xabs <= 290.32
		when xabs = 290.32 sync D goto w573;
	loc w573: invariant xabs <= 290.4
		when xabs = 290.4 sync C goto w574;
	loc w574: invariant xabs <= 290.48
		when xabs = 290.48 sync F goto w575;
	loc w575: invariant xabs <= 290.56
		when xabs = 290.56 sync E goto w576;
	loc w576: invariant xabs <= 290.8
		when xabs = 290.8 sync D goto w577;
	loc w577: invariant xabs <= 290.84
		when xabs = 290.84 sync C goto w578;
	loc w578: invariant xabs <= 291
		when xabs = 291 sync F goto w579;
	loc w579: invariant xabs <= 291.04
		when xabs = 291.04 sync E goto w580;
	loc w580: invariant xabs <= 291.28
		when xabs = 291.28 sync D goto w581;
	loc w581: invariant xabs <= 291.32
		when xabs = 291.32 sync C goto w582;
	loc w582: invariant xabs <= 291.48
		when xabs = 291.48 sync F goto w583;
	loc w583: invariant xabs <= 291.56
		when xabs = 291.56 sync E goto w584;
	loc w584: invariant xabs <= 291.76
		when xabs = 291.76 sync D goto w585;
	loc w585: invariant xabs <= 291.8
		when xabs = 291.8 sync C goto w586;
	loc w586: invariant xabs <= 292
		when xabs = 292 sync F goto w587;
	loc w587: invariant xabs <= 292.04
		when xabs = 292.04 sync E goto w588;
	loc w588: invariant xabs <= 292.24
		when xabs = 292.24 sync D goto w589;
	loc w589: invariant xabs <= 292.28
		when xabs = 292.28 sync C goto w590;
	loc w590: invariant xabs <= 292.48
		when xabs = 292.48 sync F goto w591;
	loc w591: invariant xabs <= 292.52
		when xabs = 292.52 sync E goto w592;
	loc w592: invariant xabs <= 292.72
		when xabs = 292.72 sync D goto w593;
	loc w593: invariant xabs <= 292.8
		when xabs = 292.8 sync C goto w594;
	loc w594: invariant xabs <= 292.96
		when xabs = 292.96 sync F goto w595;
	loc w595: invariant xabs <= 293
		when xabs = 293 sync E goto w596;
	loc w596: invariant xabs <= 293.24
		when xabs = 293.24 sync D goto w597;
	loc w597: invariant xabs <= 293.28
		when xabs = 293.28 sync C goto w598;
	loc w598: invariant xabs <= 293.44
		when xabs = 293.44 sync F goto w599;
	loc w599: invariant xabs <= 293.48
		when xabs = 293.48 sync E goto w600;
	loc w600: invariant xabs <= 293.72
		when xabs = 293.72 sync D goto w601;
	loc w601: invariant xabs <= 293.8
		when xabs = 293.8 sync C goto w602;
	loc w602: invariant xabs <= 293.92
		when xabs = 293.92 sync F goto w603;
	loc w603: invariant xabs <= 293.96
		when xabs = 293.96 sync E goto w604;
	loc w604: invariant xabs <= 294.24
		when xabs = 294.24 sync D goto w605;
	loc w605: invariant xabs <= 294.28
		when xabs = 294.28 sync C goto w606;
	loc w606: invariant xabs <= 294.44
		when xabs = 294.44 sync F goto w607;
	loc w607: invariant xabs <= 294.48
		when xabs = 294.48 sync E goto w608;
	loc w608: invariant xabs <= 294.72
		when xabs = 294.72 sync D goto w609;
	loc w609: invariant xabs <= 294.76
		when xabs = 294.76 sync C goto w610;
	loc w610: invariant xabs <= 294.92
		when xabs = 294.92 sync F goto w611;
	loc w611: invariant xabs <= 294.96
		when xabs = 294.96 sync E goto w612;
	loc w612: invariant xabs <= 295.2
		when xabs = 295.2 sync D goto w613;
	loc w613: invariant xabs <= 295.24
		when xabs = 295.24 sync C goto w614;
	loc w614: invariant xabs <= 295.4
		when xabs = 295.4 sync F goto w615;
	loc w615: invariant xabs <= 295.48
		when xabs = 295.48 sync E goto w616;
	loc w616: invariant xabs <= 295.68
		when xabs = 295.68 sync D goto w617;
	loc w617: invariant xabs <= 295.72
		when xabs = 295.72 sync C goto w618;
	loc w618: invariant xabs <= 295.88
		when xabs = 295.88 sync F goto w619;
	loc w619: invariant xabs <= 295.96
		when xabs = 295.96 sync E goto w620;
	loc w620: invariant xabs <= 296.2
		when xabs = 296.2 sync D goto w621;
	loc w621: invariant xabs <= 296.24
		when xabs = 296.24 sync C goto w622;
	loc w622: invariant xabs <= 296.36
		when xabs = 296.36 sync F goto w623;
	loc w623: invariant xabs <= 296.4
		when xabs = 296.4 sync E goto w624;
	loc w624: invariant xabs <= 296.68
		when xabs = 296.68 sync D goto w625;
	loc w625: invariant xabs <= 296.76
		when xabs = 296.76 sync C goto w626;
	loc w626: invariant xabs <= 296.84
		when xabs = 296.84 sync F goto w627;
	loc w627: invariant xabs <= 296.88
		when xabs = 296.88 sync E goto w628;
	loc w628: invariant xabs <= 297.16
		when xabs = 297.16 sync D goto w629;
	loc w629: invariant xabs <= 297.24
		when xabs = 297.24 sync C goto w630;
	loc w630: invariant xabs <= 297.36
		when xabs = 297.36 sync F goto w631;
	loc w631: invariant xabs <= 297.4
		when xabs = 297.4 sync E goto w632;
	loc w632: invariant xabs <= 297.64
		when xabs = 297.64 sync D goto w633;
	loc w633: invariant xabs <= 297.72
		when xabs = 297.72 sync C goto w634;
	loc w634: invariant xabs <= 297.84
		when xabs = 297.84 sync F goto w635;
	loc w635: invariant xabs <= 297.88
		when xabs = 297.88 sync E goto w636;
	loc w636: invariant xabs <= 298.16
		when xabs = 298.16 sync D goto w637;
	loc w637: invariant xabs <= 298.28
		when xabs = 298.28 sync C goto w638;
	loc w638: invariant xabs <= 298.4
		when xabs = 298.4 sync B goto w639;
	loc w639: invariant xabs <= 302.08
		when xabs = 302.08 sync A goto w640;
	loc w640: invariant xabs <= 313.52
		when xabs = 313.52 sync B goto w641;
	loc w641: invariant xabs <= 323.84
		when xabs = 323.84 sync A goto w642;
	loc w642: invariant xabs <= 324.12
		when xabs = 324.12 sync B goto w643;
	loc w643: invariant xabs <= 324.28
		when xabs = 324.28 sync A goto w644;
	loc w644: invariant xabs <= 324.64
		when xabs = 324.64 sync B goto w645;
	loc w645: invariant xabs <= 324.76
		when xabs = 324.76 sync A goto w646;
	loc w646: invariant xabs <= 325.12
		when xabs = 325.12 sync B goto w647;
	loc w647: invariant xabs <= 325.28
		when xabs = 325.28 sync A goto w648;
	loc w648: invariant xabs <= 325.64
		when xabs = 325.64 sync B goto w649;
	loc w649: invariant xabs <= 330.2
		when xabs = 330.2 sync A goto w650;
	loc w650: invariant xabs <= 330.52
		when xabs = 330.52 sync B goto w651;
	loc w651: invariant xabs <= 330.68
		when xabs = 330.68 sync A goto w652;
	loc w652: invariant xabs <= 331
		when xabs = 331 sync B goto w653;
	loc w653: invariant xabs <= 331.12
		when xabs = 331.12 sync A goto w654;
	loc w654: invariant xabs <= 332
		when xabs = 332 sync B goto w655;
	loc w655: invariant xabs <= 336.6
		when xabs = 336.6 sync A goto w656;
	loc w656: invariant xabs <= 336.84
		when xabs = 336.84 sync B goto w657;
	loc w657: invariant xabs <= 337
		when xabs = 337 sync A goto w658;
	loc w658: invariant xabs <= 337.36
		when xabs = 337.36 sync B goto w659;
	loc w659: invariant xabs <= 337.48
		when xabs = 337.48 sync A goto w660;
	loc w660: invariant xabs <= 337.84
		when xabs = 337.84 sync B goto w661;
	loc w661: invariant xabs <= 342.48
		when xabs = 342.48 sync A goto w662;
	loc w662: invariant xabs <= 342.72
		when xabs = 342.72 sync B goto w663;
	loc w663: invariant xabs <= 342.92
		when xabs = 342.92 sync A goto w664;
	loc w664: invariant xabs <= 343.24
		when xabs = 343.24 sync B goto w665;
	loc w665: invariant xabs <= 343.4
		when xabs = 343.4 sync A goto w666;
	loc w666: invariant xabs <= 343.72
		when xabs = 343.72 sync B goto w667;
	loc w667: invariant xabs <= 343.88
		when xabs = 343.88 sync A goto w668;
	loc w668: invariant xabs <= 344.24
		when xabs = 344.24 sync B goto w669;
	loc w669: invariant xabs <= 344.36
		when xabs = 344.36 sync A goto w670;
	loc w670: invariant xabs <= 344.72
		when xabs = 344.72 sync B goto w671;
	loc w671: invariant xabs <= 344.88
		when xabs = 344.88 sync A goto w672;
	loc w672: invariant xabs <= 345.16
		when xabs = 345.16 sync B goto w673;
	loc w673: invariant xabs <= 345.36
		when xabs = 345.36 sync A goto w674;
	loc w674: invariant xabs <= 345.64
		when xabs = 345.64 sync B goto w675;
	loc w675: invariant xabs <= 345.88
		when xabs = 345.88 sync A goto w676;
	loc w676: invariant xabs <= 346.16
		when xabs = 346.16 sync B goto w677;
	loc w677: invariant xabs <= 346.32
		when xabs = 346.32 sync A goto w678;
	loc w678: invariant xabs <= 346.64
		when xabs = 346.64 sync B goto w679;
	loc w679: invariant xabs <= 346.8
		when xabs = 346.8 sync A goto w680;
	loc w680: invariant xabs <= 347.16
		when xabs = 347.16 sync B goto w681;
	loc w681: invariant xabs <= 347.28
		when xabs = 347.28 sync A goto w682;
	loc w682: invariant xabs <= 347.64
		when xabs = 347.64 sync B goto w683;
	loc w683: invariant xabs <= 347.8
		when xabs = 347.8 sync A goto w684;
	loc w684: invariant xabs <= 348.12
		when xabs = 348.12 sync B goto w685;
	loc w685: invariant xabs <= 348.32
		when xabs = 348.32 sync A goto w686;
	loc w686: invariant xabs <= 348.6
		when xabs = 348.6 sync B goto w687;
	loc w687: invariant xabs <= 348.68
		when xabs = 348.68 sync A goto w688;
	loc w688: invariant xabs <= 348.72
		when xabs = 348.72 sync F goto w689;
	loc w689: invariant xabs <= 348.8
		when xabs = 348.8 sync E goto w690;
	loc w690: invariant xabs <= 349.08
		when xabs = 349.08 sync B goto w691;
	loc w691: invariant xabs <= 349.16
		when xabs = 349.16 sync A goto w692;
	loc w692: invariant xabs <= 349.24
		when xabs = 349.24 sync F goto w693;
	loc w693: invariant xabs <= 349.28
		when xabs = 349.28 sync E goto w694;
	loc w694: invariant xabs <= 349.6
		when xabs = 349.6 sync B goto w695;
	loc w695: invariant xabs <= 349.76
		when xabs = 349.76 sync A goto w696;
	loc w696: invariant xabs <= 350.08
		when xabs = 350.08 sync B goto w697;
	loc w697: invariant xabs <= 350.24
		when xabs = 350.24 sync A goto w698;
	loc w698: invariant xabs <= 350.6
		when xabs = 350.6 sync B goto w699;
	loc w699: invariant xabs <= 350.72
		when xabs = 350.72 sync A goto w700;
	loc w700: invariant xabs <= 351.04
		when xabs = 351.04 sync B goto w701;
	loc w701: invariant xabs <= 351.12
		when xabs = 351.12 sync A goto w702;
	loc w702: invariant xabs <= 351.16
		when xabs = 351.16 sync F goto w703;
	loc w703: invariant xabs <= 351.24
		when xabs = 351.24 sync E goto w704;
	loc w704: invariant xabs <= 351.52
		when xabs = 351.52 sync B goto w705;
	loc w705: invariant xabs <= 351.64
		when xabs = 351.64 sync A goto w706;
	loc w706: invariant xabs <= 351.68
		when xabs = 351.68 sync F goto w707;
	loc w707: invariant xabs <= 351.76
		when xabs = 351.76 sync E goto w708;
	loc w708: invariant xabs <= 352
		when xabs = 352 sync B goto w709;
	loc w709: invariant xabs <= 352.12
		when xabs = 352.12 sync A goto w710;
	loc w710: invariant xabs <= 352.16
		when xabs = 352.16 sync F goto w711;
	loc w711: invariant xabs <= 352.24
		when xabs = 352.24 sync E goto w712;
	loc w712: invariant xabs <= 352.52
		when xabs = 352.52 sync B goto w713;
	loc w713: invariant xabs <= 352.72
		when xabs = 352.72 sync A goto w714;
	loc w714: invariant xabs <= 353
		when xabs = 353 sync B goto w715;
	loc w715: invariant xabs <= 353.2
		when xabs = 353.2 sync A goto w716;
	loc w716: invariant xabs <= 353.52
		when xabs = 353.52 sync B goto w717;
	loc w717: invariant xabs <= 353.68
		when xabs = 353.68 sync A goto w718;
	loc w718: invariant xabs <= 354
		when xabs = 354 sync B goto w719;
	loc w719: invariant xabs <= 354.2
		when xabs = 354.2 sync A goto w720;
	loc w720: invariant xabs <= 354.48
		when xabs = 354.48 sync B goto w721;
	loc w721: invariant xabs <= 354.56
		when xabs = 354.56 sync A goto w722;
	loc w722: invariant xabs <= 354.64
		when xabs = 354.64 sync F goto w723;
	loc w723: invariant xabs <= 354.68
		when xabs = 354.68 sync E goto w724;
	loc w724: invariant xabs <= 354.96
		when xabs = 354.96 sync B goto w725;
	loc w725: invariant xabs <= 355
		when xabs = 355 sync A goto w726;
	loc w726: invariant xabs <= 355.12
		when xabs = 355.12 sync F goto w727;
	loc w727: invariant xabs <= 355.2
		when xabs = 355.2 sync E goto w728;
	loc w728: invariant xabs <= 355.44
		when xabs = 355.44 sync B goto w729;
	loc w729: invariant xabs <= 355.48
		when xabs = 355.48 sync A goto w730;
	loc w730: invariant xabs <= 355.6
		when xabs = 355.6 sync F goto w731;
	loc w731: invariant xabs <= 355.68
		when xabs = 355.68 sync E goto w732;
	loc w732: invariant xabs <= 355.92
		when xabs = 355.92 sync B goto w733;
	loc w733: invariant xabs <= 356
		when xabs = 356 sync A goto w734;
	loc w734: invariant xabs <= 356.08
		when xabs = 356.08 sync F goto w735;
	loc w735: invariant xabs <= 356.12
		when xabs = 356.12 sync E goto w736;
	loc w736: invariant xabs <= 356.44
		when xabs = 356.44 sync B goto w737;
	loc w737: invariant xabs <= 356.48
		when xabs = 356.48 sync A goto w738;
	loc w738: invariant xabs <= 356.56
		when xabs = 356.56 sync F goto w739;
	loc w739: invariant xabs <= 356.6
		when xabs = 356.6 sync E goto w740;
	loc w740: invariant xabs <= 356.92
		when xabs = 356.92 sync B goto w741;
	loc w741: invariant xabs <= 357
		when xabs = 357 sync A goto w742;
	loc w742: invariant xabs <= 357.08
		when xabs = 357.08 sync F goto w743;
	loc w743: invariant xabs <= 357.12
		when xabs = 357.12 sync E goto w744;
	loc w744: invariant xabs <= 357.4
		when xabs = 357.4 sync B goto w745;
	loc w745: invariant xabs <= 357.48
		when xabs = 357.48 sync A goto w746;
	loc w746: invariant xabs <= 357.56
		when xabs = 357.56 sync F goto w747;
	loc w747: invariant xabs <= 357.64
		when xabs = 357.64 sync E goto w748;
	loc w748: invariant xabs <= 357.88
		when xabs = 357.88 sync B goto w749;
	loc w749: invariant xabs <= 357.92
		when xabs = 357.92 sync A goto w750;
	loc w750: invariant xabs <= 358
		when xabs = 358 sync F goto w751;
	loc w751: invariant xabs <= 361.08
		when xabs = 361.08 sync E goto w752;
	loc w752: invariant xabs <= 361.28
		when xabs = 361.28 sync B goto w753;
	loc w753: invariant xabs <= 361.56
		when xabs = 361.56 sync A goto w754;
	loc w754: invariant xabs <= 361.8
		when xabs = 361.8 sync B goto w755;
	loc w755: invariant xabs <= 361.92
		when xabs = 361.92 sync A goto w756;
	loc w756: invariant xabs <= 361.96
		when xabs = 361.96 sync F goto w757;
	loc w757: invariant xabs <= 362.04
		when xabs = 362.04 sync E goto w758;
	loc w758: invariant xabs <= 362.28
		when xabs = 362.28 sync B goto w759;
	loc w759: invariant xabs <= 362.4
		when xabs = 362.4 sync A goto w760;
	loc w760: invariant xabs <= 362.44
		when xabs = 362.44 sync F goto w761;
	loc w761: invariant xabs <= 362.52
		when xabs = 362.52 sync E goto w762;
	loc w762: invariant xabs <= 362.8
		when xabs = 362.8 sync B goto w763;
	loc w763: invariant xabs <= 362.88
		when xabs = 362.88 sync A goto w764;
	loc w764: invariant xabs <= 362.92
		when xabs = 362.92 sync F goto w765;
	loc w765: invariant xabs <= 363
		when xabs = 363 sync E goto w766;
	loc w766: invariant xabs <= 363.28
		when xabs = 363.28 sync B goto w767;
	loc w767: invariant xabs <= 363.36
		when xabs = 363.36 sync A goto w768;
	loc w768: invariant xabs <= 363.44
		when xabs = 363.44 sync F goto w769;
	loc w769: invariant xabs <= 363.52
		when xabs = 363.52 sync E goto w770;
	loc w770: invariant xabs <= 363.76
		when xabs = 363.76 sync B goto w771;
	loc w771: invariant xabs <= 363.84
		when xabs = 363.84 sync A goto w772;
	loc w772: invariant xabs <= 363.96
		when xabs = 363.96 sync F goto w773;
	loc w773: invariant xabs <= 364
		when xabs = 364 sync E goto w774;
	loc w774: invariant xabs <= 364.24
		when xabs = 364.24 sync B goto w775;
	loc w775: invariant xabs <= 364.32
		when xabs = 364.32 sync A goto w776;
	loc w776: invariant xabs <= 364.44
		when xabs = 364.44 sync F goto w777;
	loc w777: invariant xabs <= 364.52
		when xabs = 364.52 sync E goto w778;
	loc w778: invariant xabs <= 364.72
		when xabs = 364.72 sync B goto w779;
	loc w779: invariant xabs <= 364.8
		when xabs = 364.8 sync A goto w780;
	loc w780: invariant xabs <= 364.96
		when xabs = 364.96 sync F goto w781;
	loc w781: invariant xabs <= 365
		when xabs = 365 sync E goto w782;
	loc w782: invariant xabs <= 365.2
		when xabs = 365.2 sync B goto w783;
	loc w783: invariant xabs <= 365.28
		when xabs = 365.28 sync A goto w784;
	loc w784: invariant xabs <= 365.44
		when xabs = 365.44 sync F goto w785;
	loc w785: invariant xabs <= 365.48
		when xabs = 365.48 sync E goto w786;
	loc w786: invariant xabs <= 365.72
		when xabs = 365.72 sync B goto w787;
	loc w787: invariant xabs <= 365.76
		when xabs = 365.76 sync A goto w788;
	loc w788: invariant xabs <= 365.92
		when xabs = 365.92 sync F goto w789;
	loc w789: invariant xabs <= 365.96
		when xabs = 365.96 sync E goto w790;
	loc w790: invariant xabs <= 366.2
		when xabs = 366.2 sync B goto w791;
	loc w791: invariant xabs <= 366.28
		when xabs = 366.28 sync A goto w792;
	loc w792: invariant xabs <= 366.4
		when xabs = 366.4 sync F goto w793;
	loc w793: invariant xabs <= 366.44
		when xabs = 366.44 sync E goto w794;
	loc w794: invariant xabs <= 366.56
		when xabs = 366.56 sync B goto w795;
	loc w795: invariant xabs <= 366.68
		when xabs = 366.68 sync C goto w796;
	loc w796: invariant xabs <= 366.76
		when xabs = 366.76 sync B goto w797;
	loc w797: invariant xabs <= 366.88
		when xabs = 366.88 sync F goto w798;
	loc w798: invariant xabs <= 366.96
		when xabs = 366.96 sync E goto w799;
	loc w799: invariant xabs <= 367.16
		when xabs = 367.16 sync C goto w800;
	loc w800: invariant xabs <= 367.24
		when xabs = 367.24 sync B goto w801;
	loc w801: invariant xabs <= 367.4
		when xabs = 367.4 sync F goto w802;
	loc w802: invariant xabs <= 367.44
		when xabs = 367.44 sync E goto w803;
	loc w803: invariant xabs <= 367.64
		when xabs = 367.64 sync C goto w804;
	loc w804: invariant xabs <= 367.68
		when xabs = 367.68 sync B goto w805;
	loc w805: invariant xabs <= 367.88
		when xabs = 367.88 sync F goto w806;
	loc w806: invariant xabs <= 367.92
		when xabs = 367.92 sync E goto w807;
	loc w807: invariant xabs <= 368.12
		when xabs = 368.12 sync C goto w808;
	loc w808: invariant xabs <= 368.2
		when xabs = 368.2 sync B goto w809;
	loc w809: invariant xabs <= 368.36
		when xabs = 368.36 sync F goto w810;
	loc w810: invariant xabs <= 368.4
		when xabs = 368.4 sync E goto w811;
	loc w811: invariant xabs <= 368.64
		when xabs = 368.64 sync C goto w812;
	loc w812: invariant xabs <= 368.68
		when xabs = 368.68 sync B goto w813;
	loc w813: invariant xabs <= 368.84
		when xabs = 368.84 sync F goto w814;
	loc w814: invariant xabs <= 368.88
		when xabs = 368.88 sync E goto w815;
	loc w815: invariant xabs <= 369.16
		when xabs = 369.16 sync C goto w816;
	loc w816: invariant xabs <= 369.2
		when xabs = 369.2 sync B goto w817;
	loc w817: invariant xabs <= 369.36
		when xabs = 369.36 sync F goto w818;
	loc w818: invariant xabs <= 369.4
		when xabs = 369.4 sync E goto w819;
	loc w819: invariant xabs <= 369.64
		when xabs = 369.64 sync C goto w820;
	loc w820: invariant xabs <= 369.68
		when xabs = 369.68 sync B goto w821;
	loc w821: invariant xabs <= 369.84
		when xabs = 369.84 sync F goto w822;
	loc w822: invariant xabs <= 369.88
		when xabs = 369.88 sync E goto w823;
	loc w823: invariant xabs <= 370.12
		when xabs = 370.12 sync C goto w824;
	loc w824: invariant xabs <= 370.16
		when xabs = 370.16 sync B goto w825;
	loc w825: invariant xabs <= 370.36
		when xabs = 370.36 sync F goto w826;
	loc w826: invariant xabs <= 370.4
		when xabs = 370.4 sync E goto w827;
	loc w827: invariant xabs <= 370.56
		when xabs = 370.56 sync C goto w828;
	loc w828: invariant xabs <= 370.64
		when xabs = 370.64 sync B goto w829;
	loc w829: invariant xabs <= 370.84
		when xabs = 370.84 sync F goto w830;
	loc w830: invariant xabs <= 370.88
		when xabs = 370.88 sync E goto w831;
	loc w831: invariant xabs <= 371.08
		when xabs = 371.08 sync C goto w832;
	loc w832: invariant xabs <= 371.12
		when xabs = 371.12 sync B goto w833;
	loc w833: invariant xabs <= 371.32
		when xabs = 371.32 sync F goto w834;
	loc w834: invariant xabs <= 371.36
		when xabs = 371.36 sync E goto w835;
	loc w835: invariant xabs <= 371.56
		when xabs = 371.56 sync C goto w836;
	loc w836: invariant xabs <= 371.64
		when xabs = 371.64 sync B goto w837;
	loc w837: invariant xabs <= 371.8
		when xabs = 371.8 sync F goto w838;
	loc w838: invariant xabs <= 371.84
		when xabs = 371.84 sync E goto w839;
	loc w839: invariant xabs <= 372.08
		when xabs = 372.08 sync C goto w840;
	loc w840: invariant xabs <= 372.12
		when xabs = 372.12 sync B goto w841;
	loc w841: invariant xabs <= 372.28
		when xabs = 372.28 sync F goto w842;
	loc w842: invariant xabs <= 372.32
		when xabs = 372.32 sync E goto w843;
	loc w843: invariant xabs <= 372.56
		when xabs = 372.56 sync C goto w844;
	loc w844: invariant xabs <= 372.6
		when xabs = 372.6 sync B goto w845;
	loc w845: invariant xabs <= 372.8
		when xabs = 372.8 sync F goto w846;
	loc w846: invariant xabs <= 372.84
		when xabs = 372.84 sync E goto w847;
	loc w847: invariant xabs <= 373.04
		when xabs = 373.04 sync C goto w848;
	loc w848: invariant xabs <= 373.08
		when xabs = 373.08 sync B goto w849;
	loc w849: invariant xabs <= 373.32
		when xabs = 373.32 sync F goto w850;
	loc w850: invariant xabs <= 373.52
		when xabs = 373.52 sync C goto w851;
	loc w851: invariant xabs <= 373.56
		when xabs = 373.56 sync B goto w852;
	loc w852: invariant xabs <= 373.8
		when xabs = 373.8 sync F goto w853;
	loc w853: invariant xabs <= 373.84
		when xabs = 373.84 sync E goto w854;
	loc w854: invariant xabs <= 374.04
		when xabs = 374.04 sync C goto w855;
	loc w855: invariant xabs <= 374.28
		when xabs = 374.28 sync F goto w856;
	loc w856: invariant xabs <= 374.32
		when xabs = 374.32 sync E goto w857;
	loc w857: invariant xabs <= 374.48
		when xabs = 374.48 sync D goto w858;
	loc w858: invariant xabs <= 374.56
		when xabs = 374.56 sync C goto w859;
	loc w859: invariant xabs <= 374.76
		when xabs = 374.76 sync F goto w860;
	loc w860: invariant xabs <= 374.8
		when xabs = 374.8 sync E goto w861;
	loc w861: invariant xabs <= 375
		when xabs = 375 sync D goto w862;
	loc w862: invariant xabs <= 375.04
		when xabs = 375.04 sync C goto w863;
	loc w863: invariant xabs <= 375.24
		when xabs = 375.24 sync F goto w864;
	loc w864: invariant xabs <= 375.28
		when xabs = 375.28 sync E goto w865;
	loc w865: invariant xabs <= 375.48
		when xabs = 375.48 sync D goto w866;
	loc w866: invariant xabs <= 375.56
		when xabs = 375.56 sync C goto w867;
	loc w867: invariant xabs <= 375.72
		when xabs = 375.72 sync F goto w868;
	loc w868: invariant xabs <= 375.76
		when xabs = 375.76 sync E goto w869;
	loc w869: invariant xabs <= 375.96
		when xabs = 375.96 sync D goto w870;
	loc w870: invariant xabs <= 376.04
		when xabs = 376.04 sync C goto w871;
	loc w871: invariant xabs <= 376.24
		when xabs = 376.24 sync F goto w872;
	loc w872: invariant xabs <= 376.28
		when xabs = 376.28 sync E goto w873;
	loc w873: invariant xabs <= 376.44
		when xabs = 376.44 sync D goto w874;
	loc w874: invariant xabs <= 376.48
		when xabs = 376.48 sync C goto w875;
	loc w875: invariant xabs <= 376.76
		when xabs = 376.76 sync F goto w876;
	loc w876: invariant xabs <= 376.8
		when xabs = 376.8 sync E goto w877;
	loc w877: invariant xabs <= 376.92
		when xabs = 376.92 sync D goto w878;
	loc w878: invariant xabs <= 376.96
		when xabs = 376.96 sync C goto w879;
	loc w879: invariant xabs <= 377.24
		when xabs = 377.24 sync F goto w880;
	loc w880: invariant xabs <= 377.28
		when xabs = 377.28 sync E goto w881;
	loc w881: invariant xabs <= 377.4
		when xabs = 377.4 sync D goto w882;
	loc w882: invariant xabs <= 377.44
		when xabs = 377.44 sync C goto w883;
	loc w883: invariant xabs <= 377.72
		when xabs = 377.72 sync F goto w884;
	loc w884: invariant xabs <= 377.76
		when xabs = 377.76 sync E goto w885;
	loc w885: invariant xabs <= 377.92
		when xabs = 377.92 sync D goto w886;
	loc w886: invariant xabs <= 377.96
		when xabs = 377.96 sync C goto w887;
	loc w887: invariant xabs <= 378
		when xabs = 378 sync F goto w888;
	loc w888: invariant xabs <= 378.16
		when xabs = 378.16 sync E goto w889;
	loc w889: invariant xabs <= 378.4
		when xabs = 378.4 sync B goto w890;
	loc w890: invariant xabs <= 380.72
		when xabs = 380.72 sync A goto w891;
	loc w891: invariant xabs <= 380.84
		when xabs = 380.84 sync B goto w892;
	loc w892: invariant xabs <= 381
		when xabs = 381 sync A goto w893;
	loc w893: invariant xabs <= 381.12
		when xabs = 381.12 sync F goto w894;
	loc w894: invariant xabs <= 381.2
		when xabs = 381.2 sync E goto w895;
	loc w895: invariant xabs <= 381.36
		when xabs = 381.36 sync B goto w896;
	loc w896: invariant xabs <= 381.44
		when xabs = 381.44 sync A goto w897;
	loc w897: invariant xabs <= 381.6
		when xabs = 381.6 sync F goto w898;
	loc w898: invariant xabs <= 381.64
		when xabs = 381.64 sync E goto w899;
	loc w899: invariant xabs <= 381.84
		when xabs = 381.84 sync B goto w900;
	loc w900: invariant xabs <= 381.92
		when xabs = 381.92 sync A goto w901;
	loc w901: invariant xabs <= 382.12
		when xabs = 382.12 sync F goto w902;
	loc w902: invariant xabs <= 382.16
		when xabs = 382.16 sync E goto w903;
	loc w903: invariant xabs <= 382.32
		when xabs = 382.32 sync B goto w904;
	loc w904: invariant xabs <= 382.36
		when xabs = 382.36 sync A goto w905;
	loc w905: invariant xabs <= 382.64
		when xabs = 382.64 sync F goto w906;
	loc w906: invariant xabs <= 382.8
		when xabs = 382.8 sync B goto w907;
	loc w907: invariant xabs <= 383.16
		when xabs = 383.16 sync A goto w908;
	loc w908: invariant xabs <= 383.64
		when xabs = 383.64 sync B goto w909;
	loc w909: invariant xabs <= 383.76
		when xabs = 383.76 sync C goto w910;
	loc w910: invariant xabs <= 384.12
		when xabs = 384.12 sync B goto w911;
	loc w911: invariant xabs <= 384.24
		when xabs = 384.24 sync C goto w912;
	loc w912: invariant xabs <= 384.28
		when xabs = 384.28 sync F goto w913;
	loc w913: invariant xabs <= 384.6
		when xabs = 384.6 sync B goto w914;
	loc w914: invariant xabs <= 384.8
		when xabs = 384.8 sync C goto w915;
	loc w915: invariant xabs <= 384.84
		when xabs = 384.84 sync B goto w916;
	loc w916: invariant xabs <= 385.08
		when xabs = 385.08 sync F goto w917;
	loc w917: invariant xabs <= 385.32
		when xabs = 385.32 sync C goto w918;
	loc w918: invariant xabs <= 385.56
		when xabs = 385.56 sync F goto w919;
	loc w919: invariant xabs <= 385.6
		when xabs = 385.6 sync E goto w920;
	loc w920: invariant xabs <= 385.72
		when xabs = 385.72 sync D goto w921;
	loc w921: invariant xabs <= 385.76
		when xabs = 385.76 sync C goto w922;
	loc w922: invariant xabs <= 387.08
		when xabs = 387.08 sync F goto w923;
	loc w923: invariant xabs <= 387.2
		when xabs = 387.2 sync D goto w924;
	loc w924: invariant xabs <= 387.56
		when xabs = 387.56 sync C goto w925;
	loc w925: invariant xabs <= 387.64
		when xabs = 387.64 sync D goto w926;
	loc w926: invariant xabs <= 387.68
		when xabs = 387.68 sync F goto w927;
	loc w927: invariant xabs <= 388.04
		when xabs = 388.04 sync C goto w928;
	loc w928: invariant xabs <= 388.2
		when xabs = 388.2 sync D goto w929;
	loc w929: invariant xabs <= 388.52
		when xabs = 388.52 sync C goto w930;
	loc w930: invariant xabs <= 388.68
		when xabs = 388.68 sync D goto w931;
	loc w931: invariant xabs <= 391
		when xabs = 391 sync C goto w932;
	loc w932: invariant xabs <= 391.48
		when xabs = 391.48 sync D goto w933;
	loc w933: invariant xabs <= 391.52
		when xabs = 391.52 sync E goto w934;
	loc w934: invariant xabs <= 392.68
		when xabs = 392.68 sync F goto w935;
	loc w935: invariant xabs <= 398
		when xabs = 398 sync H goto w936;
	loc w936: invariant xabs <= 398.08
		when xabs = 398.08 sync E goto w937;
	loc w937: invariant xabs <= 398.24
		when xabs = 398.24 sync G goto w938;
	loc w938: invariant xabs <= 398.36
		when xabs = 398.36 sync C goto w939;
	loc w939: invariant xabs <= 398.48
		when xabs = 398.48 sync B goto w940;
	loc w940: invariant xabs <= 400.4
		when xabs = 400.4 sync A goto w941;
	loc w941: invariant xabs <= 401.52
		when xabs = 401.52 sync F goto w942;
	loc w942: invariant xabs <= 403.28
		when xabs = 403.28 sync B goto w943;
	loc w943: invariant xabs <= 405.6
		when xabs = 405.6 sync C goto w944;
	loc w944: invariant xabs <= 405.68
		when xabs = 405.68 sync H goto w945;
	loc w945: invariant xabs <= 418
		when xabs = 418 sync D goto w946;
	loc w946: invariant xabs <= 418.12
		when xabs = 418.12 sync E goto w947;
	loc w947: invariant xabs <= 418.32
		when xabs = 418.32 sync G goto w948;
	loc w948: invariant xabs <= 418.44
		when xabs = 418.44 sync C goto w949;
	loc w949: invariant xabs <= 418.56
		when xabs = 418.56 sync B goto w950;
	loc w950: invariant xabs <= 420.4
		when xabs = 420.4 sync A goto w951;
	loc w951: invariant xabs <= 421.24
		when xabs = 421.24 sync F goto w952;
	loc w952: invariant xabs <= 422.76
		when xabs = 422.76 sync B goto w953;
	loc w953: invariant xabs <= 424.68
		when xabs = 424.68 sync C goto w954;
	loc w954: invariant xabs <= 424.76
		when xabs = 424.76 sync H goto w955;
	loc w955: invariant xabs <= 438
		when xabs = 438 sync D goto w956;
	loc w956: invariant xabs <= 438.12
		when xabs = 438.12 sync E goto w957;
	loc w957: invariant xabs <= 438.32
		when xabs = 438.32 sync G goto w958;
	loc w958: invariant xabs <= 438.44
		when xabs = 438.44 sync C goto w959;
	loc w959: invariant xabs <= 438.56
		when xabs = 438.56 sync B goto w960;
	loc w960: invariant xabs <= 440.4
		when xabs = 440.4 sync A goto w961;
	loc w961: invariant xabs <= 441.4
		when xabs = 441.4 sync F goto w962;
	loc w962: invariant xabs <= 442.96
		when xabs = 442.96 sync B goto w963;
	loc w963: invariant xabs <= 446.2
		when xabs = 446.2 sync C goto w964;
	loc w964: invariant xabs <= 446.28
		when xabs = 446.28 sync H goto w965;
	loc w965: invariant xabs <= 458
		when xabs = 458 sync D goto w966;
	loc w966: invariant xabs <= 458.08
		when xabs = 458.08 sync E goto w967;
	loc w967: invariant xabs <= 458.28
		when xabs = 458.28 sync G goto w968;
	loc w968: invariant xabs <= 458.4
		when xabs = 458.4 sync C goto w969;
	loc w969: invariant xabs <= 458.52
		when xabs = 458.52 sync B goto w970;
	loc w970: invariant xabs <= 460.84
		when xabs = 460.84 sync A goto w971;
	loc w971: invariant xabs <= 460.96
		when xabs = 460.96 sync F goto w972;
	loc w972: invariant xabs <= 461.16
		when xabs = 461.16 sync E goto w973;
	loc w973: invariant xabs <= 462.04
		when xabs = 462.04 sync F goto w974;
	loc w974: invariant xabs <= 462.48
		when xabs = 462.48 sync B goto w975;
	loc w975: invariant xabs <= 462.92
		when xabs = 462.92 sync C goto w976;
	loc w976: invariant xabs <= 462.96
		when xabs = 462.96 sync E goto w977;
	loc w977: invariant xabs <= 463.12
		when xabs = 463.12 sync D goto w978;
	loc w978: invariant xabs <= 463.16
		when xabs = 463.16 sync C goto w979;
	loc w979: invariant xabs <= 463.4
		when xabs = 463.4 sync F goto w980;
	loc w980: invariant xabs <= 463.44
		when xabs = 463.44 sync E goto w981;
	loc w981: invariant xabs <= 463.6
		when xabs = 463.6 sync D goto w982;
	loc w982: invariant xabs <= 463.64
		when xabs = 463.64 sync C goto w983;
	loc w983: invariant xabs <= 463.88
		when xabs = 463.88 sync F goto w984;
	loc w984: invariant xabs <= 463.92
		when xabs = 463.92 sync E goto w985;
	loc w985: invariant xabs <= 464.08
		when xabs = 464.08 sync D goto w986;
	loc w986: invariant xabs <= 464.16
		when xabs = 464.16 sync C goto w987;
	loc w987: invariant xabs <= 464.4
		when xabs = 464.4 sync F goto w988;
	loc w988: invariant xabs <= 464.44
		when xabs = 464.44 sync E goto w989;
	loc w989: invariant xabs <= 464.52
		when xabs = 464.52 sync D goto w990;
	loc w990: invariant xabs <= 464.56
		when xabs = 464.56 sync F goto w991;
	loc w991: invariant xabs <= 465.4
		when xabs = 465.4 sync C goto w992;
	loc w992: invariant xabs <= 465.44
		when xabs = 465.44 sync E goto w993;
	loc w993: invariant xabs <= 465.88
		when xabs = 465.88 sync F goto w994;
	loc w994: invariant xabs <= 466.04
		when xabs = 466.04 sync D goto w995;
	loc w995: invariant xabs <= 466.08
		when xabs = 466.08 sync C goto w996;
	loc w996: invariant xabs <= 466.36
		when xabs = 466.36 sync F goto w997;
	loc w997: invariant xabs <= 466.56
		when xabs = 466.56 sync D goto w998;
	loc w998: invariant xabs <= 466.6
		when xabs = 466.6 sync C goto w999;
	loc w999: invariant xabs <= 466.84
		when xabs = 466.84 sync F goto w1000;
	loc w1000: invariant xabs <= 467.04
		when xabs = 467.04 sync D goto w1001;
	loc w1001: invariant xabs <= 467.08
		when xabs = 467.08 sync C goto w1002;
	loc w1002: invariant xabs <= 467.36
		when xabs = 467.36 sync F goto w1003;
	loc w1003: invariant xabs <= 467.52
		when xabs = 467.52 sync D goto w1004;
	loc w1004: invariant xabs <= 467.56
		when xabs = 467.56 sync C goto w1005;
	loc w1005: invariant xabs <= 467.84
		when xabs = 467.84 sync F goto w1006;
	loc w1006: invariant xabs <= 467.88
		when xabs = 467.88 sync D goto w1007;
	loc w1007: invariant xabs <= 467.92
		when xabs = 467.92 sync E goto w1008;
	loc w1008: invariant xabs <= 468
		when xabs = 468 sync F goto w1009;
	loc w1009: invariant xabs <= 468.36
		when xabs = 468.36 sync C goto w1010;
	loc w1010: invariant xabs <= 468.48
		when xabs = 468.48 sync D goto w1011;
	loc w1011: invariant xabs <= 468.8
		when xabs = 468.8 sync C goto w1012;
	loc w1012: invariant xabs <= 468.84
		when xabs = 468.84 sync E goto w1013;
	loc w1013: invariant xabs <= 469
		when xabs = 469 sync D goto w1014;
	loc w1014: invariant xabs <= 469.04
		when xabs = 469.04 sync C goto w1015;
	loc w1015: invariant xabs <= 469.28
		when xabs = 469.28 sync F goto w1016;
	loc w1016: invariant xabs <= 469.32
		when xabs = 469.32 sync E goto w1017;
	loc w1017: invariant xabs <= 469.56
		when xabs = 469.56 sync D goto w1018;
	loc w1018: invariant xabs <= 469.76
		when xabs = 469.76 sync F goto w1019;
	loc w1019: invariant xabs <= 470.04
		when xabs = 470.04 sync E goto w1020;
	loc w1020: invariant xabs <= 470.24
		when xabs = 470.24 sync F goto w1021;
	loc w1021: invariant xabs <= 470.48
		when xabs = 470.48 sync E goto w1022;
	loc w1022: invariant xabs <= 470.52
		when xabs = 470.52 sync C goto w1023;
	loc w1023: invariant xabs <= 470.8
		when xabs = 470.8 sync F goto w1024;
	loc w1024: invariant xabs <= 470.92
		when xabs = 470.92 sync D goto w1025;
	loc w1025: invariant xabs <= 470.96
		when xabs = 470.96 sync C goto w1026;
	loc w1026: invariant xabs <= 471.28
		when xabs = 471.28 sync F goto w1027;
	loc w1027: invariant xabs <= 471.36
		when xabs = 471.36 sync D goto w1028;
	loc w1028: invariant xabs <= 471.44
		when xabs = 471.44 sync F goto w1029;
	loc w1029: invariant xabs <= 471.76
		when xabs = 471.76 sync C goto w1030;
	loc w1030: invariant xabs <= 471.92
		when xabs = 471.92 sync D goto w1031;
	loc w1031: invariant xabs <= 472.2
		when xabs = 472.2 sync C goto w1032;
	loc w1032: invariant xabs <= 472.24
		when xabs = 472.24 sync E goto w1033;
	loc w1033: invariant xabs <= 472.48
		when xabs = 472.48 sync D goto w1034;
	loc w1034: invariant xabs <= 472.68
		when xabs = 472.68 sync F goto w1035;
	loc w1035: invariant xabs <= 472.92
		when xabs = 472.92 sync E goto w1036;
	loc w1036: invariant xabs <= 473
		when xabs = 473 sync C goto w1037;
	loc w1037: invariant xabs <= 473.2
		when xabs = 473.2 sync F goto w1038;
	loc w1038: invariant xabs <= 473.4
		when xabs = 473.4 sync D goto w1039;
	loc w1039: invariant xabs <= 473.48
		when xabs = 473.48 sync C goto w1040;
	loc w1040: invariant xabs <= 473.68
		when xabs = 473.68 sync F goto w1041;
	loc w1041: invariant xabs <= 473.72
		when xabs = 473.72 sync E goto w1042;
	loc w1042: invariant xabs <= 473.96
		when xabs = 473.96 sync D goto w1043;
	loc w1043: invariant xabs <= 474.16
		when xabs = 474.16 sync F goto w1044;
	loc w1044: invariant xabs <= 474.44
		when xabs = 474.44 sync E goto w1045;
	loc w1045: invariant xabs <= 474.68
		when xabs = 474.68 sync F goto w1046;
	loc w1046: invariant xabs <= 474.92
		when xabs = 474.92 sync E goto w1047;
	loc w1047: invariant xabs <= 475.12
		when xabs = 475.12 sync F goto w1048;
	loc w1048: invariant xabs <= 475.44
		when xabs = 475.44 sync E goto w1049;
	loc w1049: invariant xabs <= 475.6
		when xabs = 475.6 sync F goto w1050;
	loc w1050: invariant xabs <= 475.88
		when xabs = 475.88 sync E goto w1051;
	loc w1051: invariant xabs <= 476.08
		when xabs = 476.08 sync F goto w1052;
	loc w1052: invariant xabs <= 476.44
		when xabs = 476.44 sync E goto w1053;
	loc w1053: invariant xabs <= 476.6
		when xabs = 476.6 sync F goto w1054;
	loc w1054: invariant xabs <= 476.88
		when xabs = 476.88 sync E goto w1055;
	loc w1055: invariant xabs <= 477.08
		when xabs = 477.08 sync F goto w1056;
	loc w1056: invariant xabs <= 477.36
		when xabs = 477.36 sync E goto w1057;
	loc w1057: invariant xabs <= 477.6
		when xabs = 477.6 sync F goto w1058;
	loc w1058: invariant xabs <= 477.88
		when xabs = 477.88 sync E goto w1059;
	loc w1059: invariant xabs <= 478
		when xabs = 478 sync F goto w1060;
	loc w1060: invariant xabs <= 478.2
		when xabs = 478.2 sync E goto w1061;
	loc w1061: invariant xabs <= 478.32
		when xabs = 478.32 sync C goto w1062;
	loc w1062: invariant xabs <= 478.44
		when xabs = 478.44 sync B goto w1063;
	loc w1063: invariant xabs <= 481.04
		when xabs = 481.04 sync A goto w1064;
	loc w1064: invariant xabs <= 481.24
		when xabs = 481.24 sync B goto w1065;
	loc w1065: invariant xabs <= 481.4
		when xabs = 481.4 sync A goto w1066;
	loc w1066: invariant xabs <= 481.44
		when xabs = 481.44 sync F goto w1067;
	loc w1067: invariant xabs <= 481.52
		when xabs = 481.52 sync E goto w1068;
	loc w1068: invariant xabs <= 481.76
		when xabs = 481.76 sync B goto w1069;
	loc w1069: invariant xabs <= 481.88
		when xabs = 481.88 sync A goto w1070;
	loc w1070: invariant xabs <= 481.92
		when xabs = 481.92 sync F goto w1071;
	loc w1071: invariant xabs <= 482
		when xabs = 482 sync E goto w1072;
	loc w1072: invariant xabs <= 482.24
		when xabs = 482.24 sync B goto w1073;
	loc w1073: invariant xabs <= 482.36
		when xabs = 482.36 sync A goto w1074;
	loc w1074: invariant xabs <= 482.44
		when xabs = 482.44 sync F goto w1075;
	loc w1075: invariant xabs <= 482.48
		when xabs = 482.48 sync E goto w1076;
	loc w1076: invariant xabs <= 482.76
		when xabs = 482.76 sync B goto w1077;
	loc w1077: invariant xabs <= 482.84
		when xabs = 482.84 sync A goto w1078;
	loc w1078: invariant xabs <= 482.92
		when xabs = 482.92 sync F goto w1079;
	loc w1079: invariant xabs <= 483
		when xabs = 483 sync E goto w1080;
	loc w1080: invariant xabs <= 483.24
		when xabs = 483.24 sync B goto w1081;
	loc w1081: invariant xabs <= 483.32
		when xabs = 483.32 sync A goto w1082;
	loc w1082: invariant xabs <= 483.44
		when xabs = 483.44 sync F goto w1083;
	loc w1083: invariant xabs <= 483.48
		when xabs = 483.48 sync E goto w1084;
	loc w1084: invariant xabs <= 483.72
		when xabs = 483.72 sync B goto w1085;
	loc w1085: invariant xabs <= 483.76
		when xabs = 483.76 sync A goto w1086;
	loc w1086: invariant xabs <= 483.92
		when xabs = 483.92 sync F goto w1087;
	loc w1087: invariant xabs <= 484
		when xabs = 484 sync E goto w1088;
	loc w1088: invariant xabs <= 484.2
		when xabs = 484.2 sync B goto w1089;
	loc w1089: invariant xabs <= 484.28
		when xabs = 484.28 sync A goto w1090;
	loc w1090: invariant xabs <= 484.4
		when xabs = 484.4 sync F goto w1091;
	loc w1091: invariant xabs <= 484.44
		when xabs = 484.44 sync E goto w1092;
	loc w1092: invariant xabs <= 484.72
		when xabs = 484.72 sync B goto w1093;
	loc w1093: invariant xabs <= 484.76
		when xabs = 484.76 sync A goto w1094;
	loc w1094: invariant xabs <= 484.88
		when xabs = 484.88 sync F goto w1095;
	loc w1095: invariant xabs <= 484.92
		when xabs = 484.92 sync E goto w1096;
	loc w1096: invariant xabs <= 485.2
		when xabs = 485.2 sync B goto w1097;
	loc w1097: invariant xabs <= 485.28
		when xabs = 485.28 sync A goto w1098;
	loc w1098: invariant xabs <= 485.36
		when xabs = 485.36 sync F goto w1099;
	loc w1099: invariant xabs <= 485.4
		when xabs = 485.4 sync E goto w1100;
	loc w1100: invariant xabs <= 485.72
		when xabs = 485.72 sync B goto w1101;
	loc w1101: invariant xabs <= 485.76
		when xabs = 485.76 sync A goto w1102;
	loc w1102: invariant xabs <= 485.88
		when xabs = 485.88 sync F goto w1103;
	loc w1103: invariant xabs <= 485.92
		when xabs = 485.92 sync E goto w1104;
	loc w1104: invariant xabs <= 486.16
		when xabs = 486.16 sync B goto w1105;
	loc w1105: invariant xabs <= 486.24
		when xabs = 486.24 sync A goto w1106;
	loc w1106: invariant xabs <= 486.4
		when xabs = 486.4 sync F goto w1107;
	loc w1107: invariant xabs <= 486.52
		when xabs = 486.52 sync B goto w1108;
	loc w1108: invariant xabs <= 486.64
		when xabs = 486.64 sync C goto w1109;
	loc w1109: invariant xabs <= 486.72
		when xabs = 486.72 sync B goto w1110;
	loc w1110: invariant xabs <= 486.84
		when xabs = 486.84 sync F goto w1111;
	loc w1111: invariant xabs <= 486.92
		when xabs = 486.92 sync E goto w1112;
	loc w1112: invariant xabs <= 487.12
		when xabs = 487.12 sync C goto w1113;
	loc w1113: invariant xabs <= 487.2
		when xabs = 487.2 sync B goto w1114;
	loc w1114: invariant xabs <= 487.36
		when xabs = 487.36 sync F goto w1115;
	loc w1115: invariant xabs <= 487.4
		when xabs = 487.4 sync E goto w1116;
	loc w1116: invariant xabs <= 487.64
		when xabs = 487.64 sync C goto w1117;
	loc w1117: invariant xabs <= 487.68
		when xabs = 487.68 sync B goto w1118;
	loc w1118: invariant xabs <= 487.84
		when xabs = 487.84 sync F goto w1119;
	loc w1119: invariant xabs <= 487.88
		when xabs = 487.88 sync E goto w1120;
	loc w1120: invariant xabs <= 488.16
		when xabs = 488.16 sync C goto w1121;
	loc w1121: invariant xabs <= 488.2
		when xabs = 488.2 sync B goto w1122;
	loc w1122: invariant xabs <= 488.28
		when xabs = 488.28 sync F goto w1123;
	loc w1123: invariant xabs <= 488.36
		when xabs = 488.36 sync E goto w1124;
	loc w1124: invariant xabs <= 488.64
		when xabs = 488.64 sync C goto w1125;
	loc w1125: invariant xabs <= 488.68
		when xabs = 488.68 sync B goto w1126;
	loc w1126: invariant xabs <= 488.8
		when xabs = 488.8 sync F goto w1127;
	loc w1127: invariant xabs <= 488.84
		when xabs = 488.84 sync E goto w1128;
	loc w1128: invariant xabs <= 489.12
		when xabs = 489.12 sync C goto w1129;
	loc w1129: invariant xabs <= 489.2
		when xabs = 489.2 sync B goto w1130;
	loc w1130: invariant xabs <= 489.28
		when xabs = 489.28 sync F goto w1131;
	loc w1131: invariant xabs <= 489.32
		when xabs = 489.32 sync E goto w1132;
	loc w1132: invariant xabs <= 489.6
		when xabs = 489.6 sync C goto w1133;
	loc w1133: invariant xabs <= 489.64
		when xabs = 489.64 sync B goto w1134;
	loc w1134: invariant xabs <= 489.8
		when xabs = 489.8 sync F goto w1135;
	loc w1135: invariant xabs <= 489.84
		when xabs = 489.84 sync E goto w1136;
	loc w1136: invariant xabs <= 490.08
		when xabs = 490.08 sync C goto w1137;
	loc w1137: invariant xabs <= 490.16
		when xabs = 490.16 sync B goto w1138;
	loc w1138: invariant xabs <= 490.28
		when xabs = 490.28 sync F goto w1139;
	loc w1139: invariant xabs <= 490.32
		when xabs = 490.32 sync E goto w1140;
	loc w1140: invariant xabs <= 490.56
		when xabs = 490.56 sync C goto w1141;
	loc w1141: invariant xabs <= 490.64
		when xabs = 490.64 sync B goto w1142;
	loc w1142: invariant xabs <= 490.76
		when xabs = 490.76 sync F goto w1143;
	loc w1143: invariant xabs <= 490.8
		when xabs = 490.8 sync E goto w1144;
	loc w1144: invariant xabs <= 491.08
		when xabs = 491.08 sync C goto w1145;
	loc w1145: invariant xabs <= 491.16
		when xabs = 491.16 sync B goto w1146;
	loc w1146: invariant xabs <= 491.24
		when xabs = 491.24 sync F goto w1147;
	loc w1147: invariant xabs <= 491.28
		when xabs = 491.28 sync E goto w1148;
	loc w1148: invariant xabs <= 491.6
		when xabs = 491.6 sync C goto w1149;
	loc w1149: invariant xabs <= 491.64
		when xabs = 491.64 sync B goto w1150;
	loc w1150: invariant xabs <= 491.72
		when xabs = 491.72 sync F goto w1151;
	loc w1151: invariant xabs <= 491.76
		when xabs = 491.76 sync E goto w1152;
	loc w1152: invariant xabs <= 492.08
		when xabs = 492.08 sync C goto w1153;
	loc w1153: invariant xabs <= 492.12
		when xabs = 492.12 sync B goto w1154;
	loc w1154: invariant xabs <= 492.2
		when xabs = 492.2 sync F goto w1155;
	loc w1155: invariant xabs <= 492.28
		when xabs = 492.28 sync E goto w1156;
	loc w1156: invariant xabs <= 492.56
		when xabs = 492.56 sync C goto w1157;
	loc w1157: invariant xabs <= 492.6
		when xabs = 492.6 sync B goto w1158;
	loc w1158: invariant xabs <= 492.72
		when xabs = 492.72 sync F goto w1159;
	loc w1159: invariant xabs <= 492.76
		when xabs = 492.76 sync E goto w1160;
	loc w1160: invariant xabs <= 493.04
		when xabs = 493.04 sync C goto w1161;
	loc w1161: invariant xabs <= 493.08
		when xabs = 493.08 sync B goto w1162;
	loc w1162: invariant xabs <= 493.2
		when xabs = 493.2 sync F goto w1163;
	loc w1163: invariant xabs <= 493.28
		when xabs = 493.28 sync E goto w1164;
	loc w1164: invariant xabs <= 493.52
		when xabs = 493.52 sync C goto w1165;
	loc w1165: invariant xabs <= 493.56
		when xabs = 493.56 sync B goto w1166;
	loc w1166: invariant xabs <= 493.72
		when xabs = 493.72 sync F goto w1167;
	loc w1167: invariant xabs <= 493.76
		when xabs = 493.76 sync E goto w1168;
	loc w1168: invariant xabs <= 494.04
		when xabs = 494.04 sync C goto w1169;
	loc w1169: invariant xabs <= 494.08
		when xabs = 494.08 sync B goto w1170;
	loc w1170: invariant xabs <= 494.16
		when xabs = 494.16 sync F goto w1171;
	loc w1171: invariant xabs <= 494.2
		when xabs = 494.2 sync E goto w1172;
	loc w1172: invariant xabs <= 494.52
		when xabs = 494.52 sync C goto w1173;
	loc w1173: invariant xabs <= 494.6
		when xabs = 494.6 sync B goto w1174;
	loc w1174: invariant xabs <= 494.64
		when xabs = 494.64 sync F goto w1175;
	loc w1175: invariant xabs <= 494.68
		when xabs = 494.68 sync E goto w1176;
	loc w1176: invariant xabs <= 495.04
		when xabs = 495.04 sync C goto w1177;
	loc w1177: invariant xabs <= 495.08
		when xabs = 495.08 sync B goto w1178;
	loc w1178: invariant xabs <= 495.12
		when xabs = 495.12 sync F goto w1179;
	loc w1179: invariant xabs <= 495.2
		when xabs = 495.2 sync E goto w1180;
	loc w1180: invariant xabs <= 495.52
		when xabs = 495.52 sync C goto w1181;
	loc w1181: invariant xabs <= 495.56
		when xabs = 495.56 sync B goto w1182;
	loc w1182: invariant xabs <= 495.64
		when xabs = 495.64 sync F goto w1183;
	loc w1183: invariant xabs <= 495.68
		when xabs = 495.68 sync E goto w1184;
	loc w1184: invariant xabs <= 495.96
		when xabs = 495.96 sync C goto w1185;
	loc w1185: invariant xabs <= 496.04
		when xabs = 496.04 sync B goto w1186;
	loc w1186: invariant xabs <= 496.16
		when xabs = 496.16 sync F goto w1187;
	loc w1187: invariant xabs <= 496.2
		when xabs = 496.2 sync E goto w1188;
	loc w1188: invariant xabs <= 496.44
		when xabs = 496.44 sync C goto w1189;
	loc w1189: invariant xabs <= 496.52
		when xabs = 496.52 sync B goto w1190;
	loc w1190: invariant xabs <= 496.64
		when xabs = 496.64 sync F goto w1191;
	loc w1191: invariant xabs <= 496.68
		when xabs = 496.68 sync E goto w1192;
	loc w1192: invariant xabs <= 496.96
		when xabs = 496.96 sync C goto w1193;
	loc w1193: invariant xabs <= 497
		when xabs = 497 sync B goto w1194;
	loc w1194: invariant xabs <= 497.12
		when xabs = 497.12 sync F goto w1195;
	loc w1195: invariant xabs <= 497.16
		when xabs = 497.16 sync E goto w1196;
	loc w1196: invariant xabs <= 497.44
		when xabs = 497.44 sync C goto w1197;
	loc w1197: invariant xabs <= 497.52
		when xabs = 497.52 sync B goto w1198;
	loc w1198: invariant xabs <= 497.56
		when xabs = 497.56 sync F goto w1199;
	loc w1199: invariant xabs <= 497.64
		when xabs = 497.64 sync E goto w1200;
	loc w1200: invariant xabs <= 497.96
		when xabs = 497.96 sync C goto w1201;
	loc w1201: invariant xabs <= 498.4
		when xabs = 498.4 sync B goto w1202;
	loc w1202: invariant xabs <= 525.08
		when xabs = 525.08 sync A goto w1203;
	loc w1203: invariant xabs <= 525.4
		when xabs = 525.4 sync B goto w1204;
	loc w1204: invariant xabs <= 525.52
		when xabs = 525.52 sync A goto w1205;
	loc w1205: invariant xabs <= 525.88
		when xabs = 525.88 sync B goto w1206;
	loc w1206: invariant xabs <= 526
		when xabs = 526 sync A goto w1207;
	loc w1207: invariant xabs <= 526.84
		when xabs = 526.84 sync B goto w1208;
	loc w1208: invariant xabs <= 530.96
		when xabs = 530.96 sync A goto w1209;
	loc w1209: invariant xabs <= 531.24
		when xabs = 531.24 sync B goto w1210;
	loc w1210: invariant xabs <= 531.44
		when xabs = 531.44 sync A goto w1211;
	loc w1211: invariant xabs <= 531.72
		when xabs = 531.72 sync B goto w1212;
	loc w1212: invariant xabs <= 531.92
		when xabs = 531.92 sync A goto w1213;
	loc w1213: invariant xabs <= 532.24
		when xabs = 532.24 sync B goto w1214;
	loc w1214: invariant xabs <= 532.4
		when xabs = 532.4 sync A goto w1215;
	loc w1215: invariant xabs <= 532.72
		when xabs = 532.72 sync B goto w1216;
	loc w1216: invariant xabs <= 532.88
		when xabs = 532.88 sync A goto w1217;
	loc w1217: invariant xabs <= 533.2
		when xabs = 533.2 sync B goto w1218;
	loc w1218: invariant xabs <= 533.4
		when xabs = 533.4 sync A goto w1219;
	loc w1219: invariant xabs <= 533.68
		when xabs = 533.68 sync B goto w1220;
	loc w1220: invariant xabs <= 533.88
		when xabs = 533.88 sync A goto w1221;
	loc w1221: invariant xabs <= 534.16
		when xabs = 534.16 sync B goto w1222;
	loc w1222: invariant xabs <= 534.4
		when xabs = 534.4 sync A goto w1223;
	loc w1223: invariant xabs <= 534.68
		when xabs = 534.68 sync B goto w1224;
	loc w1224: invariant xabs <= 534.88
		when xabs = 534.88 sync A goto w1225;
	loc w1225: invariant xabs <= 535.16
		when xabs = 535.16 sync B goto w1226;
	loc w1226: invariant xabs <= 535.32
		when xabs = 535.32 sync A goto w1227;
	loc w1227: invariant xabs <= 535.68
		when xabs = 535.68 sync B goto w1228;
	loc w1228: invariant xabs <= 535.8
		when xabs = 535.8 sync A goto w1229;
	loc w1229: invariant xabs <= 536.16
		when xabs = 536.16 sync B goto w1230;
	loc w1230: invariant xabs <= 536.32
		when xabs = 536.32 sync A goto w1231;
	loc w1231: invariant xabs <= 536.64
		when xabs = 536.64 sync B goto w1232;
	loc w1232: invariant xabs <= 536.84
		when xabs = 536.84 sync A goto w1233;
	loc w1233: invariant xabs <= 537.12
		when xabs = 537.12 sync B goto w1234;
	loc w1234: invariant xabs <= 537.2
		when xabs = 537.2 sync A goto w1235;
	loc w1235: invariant xabs <= 537.24
		when xabs = 537.24 sync F goto w1236;
	loc w1236: invariant xabs <= 537.32
		when xabs = 537.32 sync E goto w1237;
	loc w1237: invariant xabs <= 537.6
		when xabs = 537.6 sync B goto w1238;
	loc w1238: invariant xabs <= 537.64
		when xabs = 537.64 sync A goto w1239;
	loc w1239: invariant xabs <= 537.76
		when xabs = 537.76 sync F goto w1240;
	loc w1240: invariant xabs <= 537.8
		when xabs = 537.8 sync E goto w1241;
	loc w1241: invariant xabs <= 538.12
		when xabs = 538.12 sync B goto w1242;
	loc w1242: invariant xabs <= 542.72
		when xabs = 542.72 sync A goto w1243;
	loc w1243: invariant xabs <= 543
		when xabs = 543 sync B goto w1244;
	loc w1244: invariant xabs <= 543.2
		when xabs = 543.2 sync A goto w1245;
	loc w1245: invariant xabs <= 543.44
		when xabs = 543.44 sync B goto w1246;
	loc w1246: invariant xabs <= 543.6
		when xabs = 543.6 sync A goto w1247;
	loc w1247: invariant xabs <= 543.64
		when xabs = 543.64 sync F goto w1248;
	loc w1248: invariant xabs <= 543.72
		when xabs = 543.72 sync E goto w1249;
	loc w1249: invariant xabs <= 543.96
		when xabs = 543.96 sync B goto w1250;
	loc w1250: invariant xabs <= 544.04
		when xabs = 544.04 sync A goto w1251;
	loc w1251: invariant xabs <= 544.12
		when xabs = 544.12 sync F goto w1252;
	loc w1252: invariant xabs <= 544.2
		when xabs = 544.2 sync E goto w1253;
	loc w1253: invariant xabs <= 544.44
		when xabs = 544.44 sync B goto w1254;
	loc w1254: invariant xabs <= 544.52
		when xabs = 544.52 sync A goto w1255;
	loc w1255: invariant xabs <= 544.6
		when xabs = 544.6 sync F goto w1256;
	loc w1256: invariant xabs <= 544.64
		when xabs = 544.64 sync E goto w1257;
	loc w1257: invariant xabs <= 544.96
		when xabs = 544.96 sync B goto w1258;
	loc w1258: invariant xabs <= 545.04
		when xabs = 545.04 sync A goto w1259;
	loc w1259: invariant xabs <= 545.08
		when xabs = 545.08 sync F goto w1260;
	loc w1260: invariant xabs <= 545.12
		when xabs = 545.12 sync E goto w1261;
	loc w1261: invariant xabs <= 545.44
		when xabs = 545.44 sync B goto w1262;
	loc w1262: invariant xabs <= 545.52
		when xabs = 545.52 sync A goto w1263;
	loc w1263: invariant xabs <= 545.56
		when xabs = 545.56 sync F goto w1264;
	loc w1264: invariant xabs <= 545.64
		when xabs = 545.64 sync E goto w1265;
	loc w1265: invariant xabs <= 545.92
		when xabs = 545.92 sync B goto w1266;
	loc w1266: invariant xabs <= 545.96
		when xabs = 545.96 sync A goto w1267;
	loc w1267: invariant xabs <= 546.08
		when xabs = 546.08 sync F goto w1268;
	loc w1268: invariant xabs <= 546.12
		when xabs = 546.12 sync E goto w1269;
	loc w1269: invariant xabs <= 546.4
		when xabs = 546.4 sync B goto w1270;
	loc w1270: invariant xabs <= 546.48
		when xabs = 546.48 sync A goto w1271;
	loc w1271: invariant xabs <= 546.6
		when xabs = 546.6 sync F goto w1272;
	loc w1272: invariant xabs <= 546.64
		when xabs = 546.64 sync E goto w1273;
	loc w1273: invariant xabs <= 546.88
		when xabs = 546.88 sync B goto w1274;
	loc w1274: invariant xabs <= 546.96
		when xabs = 546.96 sync A goto w1275;
	loc w1275: invariant xabs <= 547.08
		when xabs = 547.08 sync F goto w1276;
	loc w1276: invariant xabs <= 547.12
		when xabs = 547.12 sync E goto w1277;
	loc w1277: invariant xabs <= 547.4
		when xabs = 547.4 sync B goto w1278;
	loc w1278: invariant xabs <= 547.48
		when xabs = 547.48 sync A goto w1279;
	loc w1279: invariant xabs <= 547.56
		when xabs = 547.56 sync F goto w1280;
	loc w1280: invariant xabs <= 547.6
		when xabs = 547.6 sync E goto w1281;
	loc w1281: invariant xabs <= 547.88
		when xabs = 547.88 sync B goto w1282;
	loc w1282: invariant xabs <= 547.96
		when xabs = 547.96 sync A goto w1283;
	loc w1283: invariant xabs <= 548.04
		when xabs = 548.04 sync F goto w1284;
	loc w1284: invariant xabs <= 548.08
		when xabs = 548.08 sync E goto w1285;
	loc w1285: invariant xabs <= 548.4
		when xabs = 548.4 sync B goto w1286;
	loc w1286: invariant xabs <= 548.44
		when xabs = 548.44 sync A goto w1287;
	loc w1287: invariant xabs <= 548.52
		when xabs = 548.52 sync F goto w1288;
	loc w1288: invariant xabs <= 548.56
		when xabs = 548.56 sync E goto w1289;
	loc w1289: invariant xabs <= 548.84
		when xabs = 548.84 sync B goto w1290;
	loc w1290: invariant xabs <= 548.92
		when xabs = 548.92 sync A goto w1291;
	loc w1291: invariant xabs <= 549.04
		when xabs = 549.04 sync F goto w1292;
	loc w1292: invariant xabs <= 549.08
		when xabs = 549.08 sync E goto w1293;
	loc w1293: invariant xabs <= 549.32
		when xabs = 549.32 sync B goto w1294;
	loc w1294: invariant xabs <= 549.4
		when xabs = 549.4 sync A goto w1295;
	loc w1295: invariant xabs <= 549.56
		when xabs = 549.56 sync F goto w1296;
	loc w1296: invariant xabs <= 549.6
		when xabs = 549.6 sync E goto w1297;
	loc w1297: invariant xabs <= 549.8
		when xabs = 549.8 sync B goto w1298;
	loc w1298: invariant xabs <= 549.88
		when xabs = 549.88 sync A goto w1299;
	loc w1299: invariant xabs <= 550.04
		when xabs = 550.04 sync F goto w1300;
	loc w1300: invariant xabs <= 550.08
		when xabs = 550.08 sync E goto w1301;
	loc w1301: invariant xabs <= 550.2
		when xabs = 550.2 sync B goto w1302;
	loc w1302: invariant xabs <= 550.32
		when xabs = 550.32 sync C goto w1303;
	loc w1303: invariant xabs <= 550.4
		when xabs = 550.4 sync B goto w1304;
	loc w1304: invariant xabs <= 550.48
		when xabs = 550.48 sync F goto w1305;
	loc w1305: invariant xabs <= 550.56
		when xabs = 550.56 sync E goto w1306;
	loc w1306: invariant xabs <= 550.8
		when xabs = 550.8 sync C goto w1307;
	loc w1307: invariant xabs <= 550.88
		when xabs = 550.88 sync B goto w1308;
	loc w1308: invariant xabs <= 550.96
		when xabs = 550.96 sync F goto w1309;
	loc w1309: invariant xabs <= 551.04
		when xabs = 551.04 sync E goto w1310;
	loc w1310: invariant xabs <= 551.32
		when xabs = 551.32 sync C goto w1311;
	loc w1311: invariant xabs <= 551.4
		when xabs = 551.4 sync B goto w1312;
	loc w1312: invariant xabs <= 551.44
		when xabs = 551.44 sync F goto w1313;
	loc w1313: invariant xabs <= 551.52
		when xabs = 551.52 sync E goto w1314;
	loc w1314: invariant xabs <= 551.8
		when xabs = 551.8 sync C goto w1315;
	loc w1315: invariant xabs <= 551.88
		when xabs = 551.88 sync B goto w1316;
	loc w1316: invariant xabs <= 551.96
		when xabs = 551.96 sync F goto w1317;
	loc w1317: invariant xabs <= 552
		when xabs = 552 sync E goto w1318;
	loc w1318: invariant xabs <= 552.28
		when xabs = 552.28 sync C goto w1319;
	loc w1319: invariant xabs <= 552.36
		when xabs = 552.36 sync B goto w1320;
	loc w1320: invariant xabs <= 552.48
		when xabs = 552.48 sync F goto w1321;
	loc w1321: invariant xabs <= 552.52
		when xabs = 552.52 sync E goto w1322;
	loc w1322: invariant xabs <= 552.76
		when xabs = 552.76 sync C goto w1323;
	loc w1323: invariant xabs <= 552.8
		when xabs = 552.8 sync B goto w1324;
	loc w1324: invariant xabs <= 552.96
		when xabs = 552.96 sync F goto w1325;
	loc w1325: invariant xabs <= 553.04
		when xabs = 553.04 sync E goto w1326;
	loc w1326: invariant xabs <= 553.24
		when xabs = 553.24 sync C goto w1327;
	loc w1327: invariant xabs <= 553.32
		when xabs = 553.32 sync B goto w1328;
	loc w1328: invariant xabs <= 553.44
		when xabs = 553.44 sync F goto w1329;
	loc w1329: invariant xabs <= 553.52
		when xabs = 553.52 sync E goto w1330;
	loc w1330: invariant xabs <= 553.72
		when xabs = 553.72 sync C goto w1331;
	loc w1331: invariant xabs <= 553.8
		when xabs = 553.8 sync B goto w1332;
	loc w1332: invariant xabs <= 553.92
		when xabs = 553.92 sync F goto w1333;
	loc w1333: invariant xabs <= 554
		when xabs = 554 sync E goto w1334;
	loc w1334: invariant xabs <= 554.24
		when xabs = 554.24 sync C goto w1335;
	loc w1335: invariant xabs <= 554.32
		when xabs = 554.32 sync B goto w1336;
	loc w1336: invariant xabs <= 554.4
		when xabs = 554.4 sync F goto w1337;
	loc w1337: invariant xabs <= 554.48
		when xabs = 554.48 sync E goto w1338;
	loc w1338: invariant xabs <= 554.72
		when xabs = 554.72 sync C goto w1339;
	loc w1339: invariant xabs <= 554.8
		when xabs = 554.8 sync B goto w1340;
	loc w1340: invariant xabs <= 554.92
		when xabs = 554.92 sync F goto w1341;
	loc w1341: invariant xabs <= 554.96
		when xabs = 554.96 sync E goto w1342;
	loc w1342: invariant xabs <= 555.2
		when xabs = 555.2 sync C goto w1343;
	loc w1343: invariant xabs <= 555.28
		when xabs = 555.28 sync B goto w1344;
	loc w1344: invariant xabs <= 555.4
		when xabs = 555.4 sync F goto w1345;
	loc w1345: invariant xabs <= 555.48
		when xabs = 555.48 sync E goto w1346;
	loc w1346: invariant xabs <= 555.68
		when xabs = 555.68 sync C goto w1347;
	loc w1347: invariant xabs <= 555.76
		when xabs = 555.76 sync B goto w1348;
	loc w1348: invariant xabs <= 555.92
		when xabs = 555.92 sync F goto w1349;
	loc w1349: invariant xabs <= 555.96
		when xabs = 555.96 sync E goto w1350;
	loc w1350: invariant xabs <= 556.16
		when xabs = 556.16 sync C goto w1351;
	loc w1351: invariant xabs <= 556.2
		when xabs = 556.2 sync B goto w1352;
	loc w1352: invariant xabs <= 556.4
		when xabs = 556.4 sync F goto w1353;
	loc w1353: invariant xabs <= 556.44
		when xabs = 556.44 sync E goto w1354;
	loc w1354: invariant xabs <= 556.68
		when xabs = 556.68 sync C goto w1355;
	loc w1355: invariant xabs <= 556.72
		when xabs = 556.72 sync B goto w1356;
	loc w1356: invariant xabs <= 556.88
		when xabs = 556.88 sync F goto w1357;
	loc w1357: invariant xabs <= 556.92
		when xabs = 556.92 sync E goto w1358;
	loc w1358: invariant xabs <= 557.16
		when xabs = 557.16 sync C goto w1359;
	loc w1359: invariant xabs <= 557.2
		when xabs = 557.2 sync B goto w1360;
	loc w1360: invariant xabs <= 557.36
		when xabs = 557.36 sync F goto w1361;
	loc w1361: invariant xabs <= 557.4
		when xabs = 557.4 sync E goto w1362;
	loc w1362: invariant xabs <= 557.68
		when xabs = 557.68 sync C goto w1363;
	loc w1363: invariant xabs <= 557.72
		when xabs = 557.72 sync B goto w1364;
	loc w1364: invariant xabs <= 557.88
		when xabs = 557.88 sync F goto w1365;
	loc w1365: invariant xabs <= 557.92
		when xabs = 557.92 sync E goto w1366;
	loc w1366: invariant xabs <= 558.16
		when xabs = 558.16 sync C goto w1367;
	loc w1367: invariant xabs <= 558.28
		when xabs = 558.28 sync B goto w1368;
	loc w1368: invariant xabs <= 561.36
		when xabs = 561.36 sync A goto w1369;
	loc w1369: invariant xabs <= 561.56
		when xabs = 561.56 sync B goto w1370;
	loc w1370: invariant xabs <= 561.72
		when xabs = 561.72 sync A goto w1371;
	loc w1371: invariant xabs <= 561.76
		when xabs = 561.76 sync F goto w1372;
	loc w1372: invariant xabs <= 561.84
		when xabs = 561.84 sync E goto w1373;
	loc w1373: invariant xabs <= 562.04
		when xabs = 562.04 sync B goto w1374;
	loc w1374: invariant xabs <= 562.16
		when xabs = 562.16 sync A goto w1375;
	loc w1375: invariant xabs <= 562.32
		when xabs = 562.32 sync F goto w1376;
	loc w1376: invariant xabs <= 562.36
		when xabs = 562.36 sync E goto w1377;
	loc w1377: invariant xabs <= 562.52
		when xabs = 562.52 sync B goto w1378;
	loc w1378: invariant xabs <= 562.6
		when xabs = 562.6 sync A goto w1379;
	loc w1379: invariant xabs <= 562.8
		when xabs = 562.8 sync F goto w1380;
	loc w1380: invariant xabs <= 562.84
		when xabs = 562.84 sync E goto w1381;
	loc w1381: invariant xabs <= 563
		when xabs = 563 sync B goto w1382;
	loc w1382: invariant xabs <= 563.08
		when xabs = 563.08 sync A goto w1383;
	loc w1383: invariant xabs <= 563.28
		when xabs = 563.28 sync F goto w1384;
	loc w1384: invariant xabs <= 563.32
		when xabs = 563.32 sync E goto w1385;
	loc w1385: invariant xabs <= 563.6
		when xabs = 563.6 sync B goto w1386;
	loc w1386: invariant xabs <= 563.76
		when xabs = 563.76 sync F goto w1387;
	loc w1387: invariant xabs <= 563.8
		when xabs = 563.8 sync E goto w1388;
	loc w1388: invariant xabs <= 564
		when xabs = 564 sync C goto w1389;
	loc w1389: invariant xabs <= 564.08
		when xabs = 564.08 sync B goto w1390;
	loc w1390: invariant xabs <= 564.24
		when xabs = 564.24 sync F goto w1391;
	loc w1391: invariant xabs <= 564.28
		when xabs = 564.28 sync E goto w1392;
	loc w1392: invariant xabs <= 564.48
		when xabs = 564.48 sync C goto w1393;
	loc w1393: invariant xabs <= 564.56
		when xabs = 564.56 sync B goto w1394;
	loc w1394: invariant xabs <= 564.76
		when xabs = 564.76 sync F goto w1395;
	loc w1395: invariant xabs <= 564.8
		when xabs = 564.8 sync E goto w1396;
	loc w1396: invariant xabs <= 564.96
		when xabs = 564.96 sync C goto w1397;
	loc w1397: invariant xabs <= 565.04
		when xabs = 565.04 sync B goto w1398;
	loc w1398: invariant xabs <= 565.28
		when xabs = 565.28 sync F goto w1399;
	loc w1399: invariant xabs <= 565.32
		when xabs = 565.32 sync E goto w1400;
	loc w1400: invariant xabs <= 565.44
		when xabs = 565.44 sync C goto w1401;
	loc w1401: invariant xabs <= 565.48
		when xabs = 565.48 sync B goto w1402;
	loc w1402: invariant xabs <= 565.76
		when xabs = 565.76 sync F goto w1403;
	loc w1403: invariant xabs <= 565.8
		when xabs = 565.8 sync E goto w1404;
	loc w1404: invariant xabs <= 565.92
		when xabs = 565.92 sync C goto w1405;
	loc w1405: invariant xabs <= 565.96
		when xabs = 565.96 sync B goto w1406;
	loc w1406: invariant xabs <= 566.24
		when xabs = 566.24 sync F goto w1407;
	loc w1407: invariant xabs <= 566.28
		when xabs = 566.28 sync E goto w1408;
	loc w1408: invariant xabs <= 566.44
		when xabs = 566.44 sync C goto w1409;
	loc w1409: invariant xabs <= 566.48
		when xabs = 566.48 sync B goto w1410;
	loc w1410: invariant xabs <= 566.72
		when xabs = 566.72 sync F goto w1411;
	loc w1411: invariant xabs <= 566.92
		when xabs = 566.92 sync C goto w1412;
	loc w1412: invariant xabs <= 567
		when xabs = 567 sync B goto w1413;
	loc w1413: invariant xabs <= 567.2
		when xabs = 567.2 sync F goto w1414;
	loc w1414: invariant xabs <= 567.24
		when xabs = 567.24 sync E goto w1415;
	loc w1415: invariant xabs <= 567.44
		when xabs = 567.44 sync C goto w1416;
	loc w1416: invariant xabs <= 567.48
		when xabs = 567.48 sync B goto w1417;
	loc w1417: invariant xabs <= 567.68
		when xabs = 567.68 sync F goto w1418;
	loc w1418: invariant xabs <= 567.72
		when xabs = 567.72 sync E goto w1419;
	loc w1419: invariant xabs <= 567.88
		when xabs = 567.88 sync C goto w1420;
	loc w1420: invariant xabs <= 567.96
		when xabs = 567.96 sync B goto w1421;
	loc w1421: invariant xabs <= 568.24
		when xabs = 568.24 sync F goto w1422;
	loc w1422: invariant xabs <= 568.32
		when xabs = 568.32 sync C goto w1423;
	loc w1423: invariant xabs <= 568.36
		when xabs = 568.36 sync F goto w1424;
	loc w1424: invariant xabs <= 568.72
		when xabs = 568.72 sync B goto w1425;
	loc w1425: invariant xabs <= 569.2
		when xabs = 569.2 sync C goto w1426;
	loc w1426: invariant xabs <= 569.24
		when xabs = 569.24 sync E goto w1427;
	loc w1427: invariant xabs <= 569.36
		when xabs = 569.36 sync D goto w1428;
	loc w1428: invariant xabs <= 569.4
		when xabs = 569.4 sync C goto w1429;
	loc w1429: invariant xabs <= 569.68
		when xabs = 569.68 sync F goto w1430;
	loc w1430: invariant xabs <= 569.88
		when xabs = 569.88 sync D goto w1431;
	loc w1431: invariant xabs <= 569.92
		when xabs = 569.92 sync C goto w1432;
	loc w1432: invariant xabs <= 570.16
		when xabs = 570.16 sync F goto w1433;
	loc w1433: invariant xabs <= 570.36
		when xabs = 570.36 sync D goto w1434;
	loc w1434: invariant xabs <= 570.4
		when xabs = 570.4 sync C goto w1435;
	loc w1435: invariant xabs <= 570.64
		when xabs = 570.64 sync F goto w1436;
	loc w1436: invariant xabs <= 570.68
		when xabs = 570.68 sync E goto w1437;
	loc w1437: invariant xabs <= 570.84
		when xabs = 570.84 sync D goto w1438;
	loc w1438: invariant xabs <= 570.88
		when xabs = 570.88 sync C goto w1439;
	loc w1439: invariant xabs <= 571.16
		when xabs = 571.16 sync F goto w1440;
	loc w1440: invariant xabs <= 571.28
		when xabs = 571.28 sync E goto w1441;
	loc w1441: invariant xabs <= 572.16
		when xabs = 572.16 sync F goto w1442;
	loc w1442: invariant xabs <= 572.28
		when xabs = 572.28 sync D goto w1443;
	loc w1443: invariant xabs <= 572.64
		when xabs = 572.64 sync C goto w1444;
	loc w1444: invariant xabs <= 572.8
		when xabs = 572.8 sync D goto w1445;
	loc w1445: invariant xabs <= 573.08
		when xabs = 573.08 sync C goto w1446;
	loc w1446: invariant xabs <= 573.12
		when xabs = 573.12 sync E goto w1447;
	loc w1447: invariant xabs <= 573.28
		when xabs = 573.28 sync D goto w1448;
	loc w1448: invariant xabs <= 573.36
		when xabs = 573.36 sync C goto w1449;
	loc w1449: invariant xabs <= 573.6
		when xabs = 573.6 sync F goto w1450;
	loc w1450: invariant xabs <= 573.76
		when xabs = 573.76 sync D goto w1451;
	loc w1451: invariant xabs <= 573.84
		when xabs = 573.84 sync C goto w1452;
	loc w1452: invariant xabs <= 574.12
		when xabs = 574.12 sync F goto w1453;
	loc w1453: invariant xabs <= 574.16
		when xabs = 574.16 sync D goto w1454;
	loc w1454: invariant xabs <= 574.24
		when xabs = 574.24 sync F goto w1455;
	loc w1455: invariant xabs <= 576.08
		when xabs = 576.08 sync C goto w1456;
	loc w1456: invariant xabs <= 576.52
		when xabs = 576.52 sync D goto w1457;
	loc w1457: invariant xabs <= 576.76
		when xabs = 576.76 sync E goto w1458;
	loc w1458: invariant xabs <= 577.04
		when xabs = 577.04 sync F goto w1459;
	loc w1459: invariant xabs <= 577.12
		when xabs = 577.12 sync E goto w1460;
	loc w1460: invariant xabs <= 578
		when xabs = 578 sync F goto w1461;
	loc w1461: invariant xabs <= 578.2
		when xabs = 578.2 sync E goto w1462;
	loc w1462: invariant xabs <= 578.32
		when xabs = 578.32 sync C goto w1463;
	loc w1463: invariant xabs <= 578.44
		when xabs = 578.44 sync B goto w1464;
	loc w1464: invariant xabs <= 580.6
		when xabs = 580.6 sync A goto w1465;
	loc w1465: invariant xabs <= 581.48
		when xabs = 581.48 sync F goto w1466;
	loc w1466: invariant xabs <= 582.44
		when xabs = 582.44 sync B goto w1467;
	loc w1467: invariant xabs <= 585.88
		when xabs = 585.88 sync C goto w1468;
	loc w1468: invariant xabs <= 587.36
		when xabs = 587.36 sync D goto w1469;
	loc w1469: invariant xabs <= 598
		when xabs = 598 sync H goto w1470;
	loc w1470: invariant xabs <= 598.12
		when xabs = 598.12 sync E goto w1471;
	loc w1471: invariant xabs <= 598.28
		when xabs = 598.28 sync G goto w1472;
	loc w1472: invariant xabs <= 598.4
		when xabs = 598.4 sync C goto w1473;
	loc w1473: invariant xabs <= 598.52
		when xabs = 598.52 sync B goto w1474;
	loc w1474: invariant xabs <= 600.36
		when xabs = 600.36 sync A goto w1475;
	loc w1475: invariant xabs <= 601.16
		when xabs = 601.16 sync F goto w1476;
	loc w1476: invariant xabs <= 602.68
		when xabs = 602.68 sync B goto w1477;
	loc w1477: invariant xabs <= 605.2
		when xabs = 605.2 sync C goto w1478;
	loc w1478: invariant xabs <= 605.28
		when xabs = 605.28 sync H goto w1479;
	loc w1479: invariant xabs <= 618
		when xabs = 618 sync D goto w1480;
	loc w1480: invariant xabs <= 618.12
		when xabs = 618.12 sync E goto w1481;
	loc w1481: invariant xabs <= 618.32
		when xabs = 618.32 sync G goto w1482;
	loc w1482: invariant xabs <= 618.44
		when xabs = 618.44 sync C goto w1483;
	loc w1483: invariant xabs <= 618.56
		when xabs = 618.56 sync B goto w1484;
	loc w1484: invariant xabs <= 620.36
		when xabs = 620.36 sync A goto w1485;
	loc w1485: invariant xabs <= 621.36
		when xabs = 621.36 sync F goto w1486;
	loc w1486: invariant xabs <= 623
		when xabs = 623 sync B goto w1487;
	loc w1487: invariant xabs <= 625.28
		when xabs = 625.28 sync C goto w1488;
	loc w1488: invariant xabs <= 625.36
		when xabs = 625.36 sync H goto w1489;
	loc w1489: invariant xabs <= 638
		when xabs = 638 sync D goto w1490;
	loc w1490: invariant xabs <= 638.12
		when xabs = 638.12 sync E goto w1491;
	loc w1491: invariant xabs <= 638.32
		when xabs = 638.32 sync G goto w1492;
	loc w1492: invariant xabs <= 638.44
		when xabs = 638.44 sync C goto w1493;
	loc w1493: invariant xabs <= 638.56
		when xabs = 638.56 sync B goto w1494;
	loc w1494: invariant xabs <= 640.36
		when xabs = 640.36 sync A goto w1495;
	loc w1495: invariant xabs <= 641.48
		when xabs = 641.48 sync F goto w1496;
	loc w1496: invariant xabs <= 642.68
		when xabs = 642.68 sync B goto w1497;
	loc w1497: invariant xabs <= 645.12
		when xabs = 645.12 sync C goto w1498;
	loc w1498: invariant xabs <= 645.6
		when xabs = 645.6 sync D goto w1499;
	loc w1499: invariant xabs <= 645.68
		when xabs = 645.68 sync E goto w1500;
	loc w1500: invariant xabs <= 646.08
		when xabs = 646.08 sync F goto w1501;
	loc w1501: invariant xabs <= 646.12
		when xabs = 646.12 sync E goto w1502;
	loc w1502: invariant xabs <= 648.52
		when xabs = 648.52 sync F goto w1503;
	loc w1503: invariant xabs <= 648.72
		when xabs = 648.72 sync E goto w1504;
	loc w1504: invariant xabs <= 649
		when xabs = 649 sync F goto w1505;
	loc w1505: invariant xabs <= 649.16
		when xabs = 649.16 sync E goto w1506;
	loc w1506: invariant xabs <= 649.76
		when xabs = 649.76 sync F goto w1507;
	loc w1507: invariant xabs <= 651.48
		when xabs = 651.48 sync H goto w1508;
	loc w1508: invariant xabs <= 651.64
		when xabs = 651.64 sync E goto w1509;
	loc w1509: invariant xabs <= 651.96
		when xabs = 651.96 sync F goto w1510;
	loc w1510: invariant xabs <= 652.16
		when xabs = 652.16 sync E goto w1511;
	loc w1511: invariant xabs <= 652.44
		when xabs = 652.44 sync F goto w1512;
	loc w1512: invariant xabs <= 652.64
		when xabs = 652.64 sync E goto w1513;
	loc w1513: invariant xabs <= 654.4
		when xabs = 654.4 sync F goto w1514;
	loc w1514: invariant xabs <= 654.64
		when xabs = 654.64 sync E goto w1515;
	loc w1515: invariant xabs <= 654.88
		when xabs = 654.88 sync F goto w1516;
	loc w1516: invariant xabs <= 655.12
		when xabs = 655.12 sync E goto w1517;
	loc w1517: invariant xabs <= 655.36
		when xabs = 655.36 sync F goto w1518;
	loc w1518: invariant xabs <= 655.6
		when xabs = 655.6 sync E goto w1519;
	loc w1519: invariant xabs <= 655.88
		when xabs = 655.88 sync F goto w1520;
	loc w1520: invariant xabs <= 656.04
		when xabs = 656.04 sync E goto w1521;
	loc w1521: invariant xabs <= 656.88
		when xabs = 656.88 sync F goto w1522;
	loc w1522: invariant xabs <= 656.92
		when xabs = 656.92 sync E goto w1523;
	loc w1523: invariant xabs <= 657.32
		when xabs = 657.32 sync F goto w1524;
	loc w1524: invariant xabs <= 657.56
		when xabs = 657.56 sync E goto w1525;
	loc w1525: invariant xabs <= 657.8
		when xabs = 657.8 sync F goto w1526;
	loc w1526: invariant xabs <= 658.04
		when xabs = 658.04 sync E goto w1527;
	loc w1527: invariant xabs <= 658.24
		when xabs = 658.24 sync G goto w1528;
	loc w1528: invariant xabs <= 658.36
		when xabs = 658.36 sync C goto w1529;
	loc w1529: invariant xabs <= 658.48
		when xabs = 658.48 sync B goto w1530;
	loc w1530: invariant xabs <= 661.72
		when xabs = 661.72 sync A goto w1531;
	loc w1531: invariant xabs <= 661.92
		when xabs = 661.92 sync B goto w1532;
	loc w1532: invariant xabs <= 662.12
		when xabs = 662.12 sync A goto w1533;
	loc w1533: invariant xabs <= 662.16
		when xabs = 662.16 sync F goto w1534;
	loc w1534: invariant xabs <= 662.24
		when xabs = 662.24 sync E goto w1535;
	loc w1535: invariant xabs <= 662.4
		when xabs = 662.4 sync B goto w1536;
	loc w1536: invariant xabs <= 662.52
		when xabs = 662.52 sync A goto w1537;
	loc w1537: invariant xabs <= 662.68
		when xabs = 662.68 sync F goto w1538;
	loc w1538: invariant xabs <= 662.72
		when xabs = 662.72 sync E goto w1539;
	loc w1539: invariant xabs <= 662.88
		when xabs = 662.88 sync B goto w1540;
	loc w1540: invariant xabs <= 662.96
		when xabs = 662.96 sync A goto w1541;
	loc w1541: invariant xabs <= 663.16
		when xabs = 663.16 sync F goto w1542;
	loc w1542: invariant xabs <= 663.2
		when xabs = 663.2 sync E goto w1543;
	loc w1543: invariant xabs <= 663.4
		when xabs = 663.4 sync B goto w1544;
	loc w1544: invariant xabs <= 663.44
		when xabs = 663.44 sync A goto w1545;
	loc w1545: invariant xabs <= 663.68
		when xabs = 663.68 sync F goto w1546;
	loc w1546: invariant xabs <= 663.96
		when xabs = 663.96 sync B goto w1547;
	loc w1547: invariant xabs <= 664.12
		when xabs = 664.12 sync F goto w1548;
	loc w1548: invariant xabs <= 664.16
		when xabs = 664.16 sync E goto w1549;
	loc w1549: invariant xabs <= 664.4
		when xabs = 664.4 sync C goto w1550;
	loc w1550: invariant xabs <= 664.48
		when xabs = 664.48 sync B goto w1551;
	loc w1551: invariant xabs <= 664.6
		when xabs = 664.6 sync F goto w1552;
	loc w1552: invariant xabs <= 664.64
		when xabs = 664.64 sync E goto w1553;
	loc w1553: invariant xabs <= 664.88
		when xabs = 664.88 sync C goto w1554;
	loc w1554: invariant xabs <= 664.96
		when xabs = 664.96 sync B goto w1555;
	loc w1555: invariant xabs <= 665.12
		when xabs = 665.12 sync F goto w1556;
	loc w1556: invariant xabs <= 665.16
		when xabs = 665.16 sync E goto w1557;
	loc w1557: invariant xabs <= 665.36
		when xabs = 665.36 sync C goto w1558;
	loc w1558: invariant xabs <= 665.4
		when xabs = 665.4 sync B goto w1559;
	loc w1559: invariant xabs <= 665.6
		when xabs = 665.6 sync F goto w1560;
	loc w1560: invariant xabs <= 665.64
		when xabs = 665.64 sync E goto w1561;
	loc w1561: invariant xabs <= 665.84
		when xabs = 665.84 sync C goto w1562;
	loc w1562: invariant xabs <= 665.88
		when xabs = 665.88 sync B goto w1563;
	loc w1563: invariant xabs <= 666.12
		when xabs = 666.12 sync F goto w1564;
	loc w1564: invariant xabs <= 666.16
		when xabs = 666.16 sync E goto w1565;
	loc w1565: invariant xabs <= 666.32
		when xabs = 666.32 sync C goto w1566;
	loc w1566: invariant xabs <= 666.36
		when xabs = 666.36 sync B goto w1567;
	loc w1567: invariant xabs <= 666.6
		when xabs = 666.6 sync F goto w1568;
	loc w1568: invariant xabs <= 666.64
		when xabs = 666.64 sync E goto w1569;
	loc w1569: invariant xabs <= 666.84
		when xabs = 666.84 sync C goto w1570;
	loc w1570: invariant xabs <= 666.88
		when xabs = 666.88 sync B goto w1571;
	loc w1571: invariant xabs <= 667.04
		when xabs = 667.04 sync F goto w1572;
	loc w1572: invariant xabs <= 667.12
		when xabs = 667.12 sync E goto w1573;
	loc w1573: invariant xabs <= 667.32
		when xabs = 667.32 sync C goto w1574;
	loc w1574: invariant xabs <= 667.4
		when xabs = 667.4 sync B goto w1575;
	loc w1575: invariant xabs <= 667.52
		when xabs = 667.52 sync F goto w1576;
	loc w1576: invariant xabs <= 667.6
		when xabs = 667.6 sync E goto w1577;
	loc w1577: invariant xabs <= 667.84
		when xabs = 667.84 sync C goto w1578;
	loc w1578: invariant xabs <= 667.88
		when xabs = 667.88 sync B goto w1579;
	loc w1579: invariant xabs <= 668.04
		when xabs = 668.04 sync F goto w1580;
	loc w1580: invariant xabs <= 668.08
		when xabs = 668.08 sync E goto w1581;
	loc w1581: invariant xabs <= 668.32
		when xabs = 668.32 sync C goto w1582;
	loc w1582: invariant xabs <= 668.36
		when xabs = 668.36 sync B goto w1583;
	loc w1583: invariant xabs <= 668.56
		when xabs = 668.56 sync F goto w1584;
	loc w1584: invariant xabs <= 668.6
		when xabs = 668.6 sync E goto w1585;
	loc w1585: invariant xabs <= 668.8
		when xabs = 668.8 sync C goto w1586;
	loc w1586: invariant xabs <= 668.84
		when xabs = 668.84 sync B goto w1587;
	loc w1587: invariant xabs <= 669.04
		when xabs = 669.04 sync F goto w1588;
	loc w1588: invariant xabs <= 669.08
		when xabs = 669.08 sync E goto w1589;
	loc w1589: invariant xabs <= 669.28
		when xabs = 669.28 sync C goto w1590;
	loc w1590: invariant xabs <= 669.32
		when xabs = 669.32 sync B goto w1591;
	loc w1591: invariant xabs <= 669.52
		when xabs = 669.52 sync F goto w1592;
	loc w1592: invariant xabs <= 669.56
		when xabs = 669.56 sync E goto w1593;
	loc w1593: invariant xabs <= 669.76
		when xabs = 669.76 sync C goto w1594;
	loc w1594: invariant xabs <= 669.84
		when xabs = 669.84 sync B goto w1595;
	loc w1595: invariant xabs <= 670
		when xabs = 670 sync F goto w1596;
	loc w1596: invariant xabs <= 670.04
		when xabs = 670.04 sync E goto w1597;
	loc w1597: invariant xabs <= 670.16
		when xabs = 670.16 sync C goto w1598;
	loc w1598: invariant xabs <= 670.28
		when xabs = 670.28 sync D goto w1599;
	loc w1599: invariant xabs <= 670.32
		when xabs = 670.32 sync C goto w1600;
	loc w1600: invariant xabs <= 670.44
		when xabs = 670.44 sync F goto w1601;
	loc w1601: invariant xabs <= 670.52
		when xabs = 670.52 sync E goto w1602;
	loc w1602: invariant xabs <= 670.76
		when xabs = 670.76 sync D goto w1603;
	loc w1603: invariant xabs <= 670.84
		when xabs = 670.84 sync C goto w1604;
	loc w1604: invariant xabs <= 670.96
		when xabs = 670.96 sync F goto w1605;
	loc w1605: invariant xabs <= 671
		when xabs = 671 sync E goto w1606;
	loc w1606: invariant xabs <= 671.24
		when xabs = 671.24 sync D goto w1607;
	loc w1607: invariant xabs <= 671.32
		when xabs = 671.32 sync C goto w1608;
	loc w1608: invariant xabs <= 671.44
		when xabs = 671.44 sync F goto w1609;
	loc w1609: invariant xabs <= 671.52
		when xabs = 671.52 sync E goto w1610;
	loc w1610: invariant xabs <= 671.72
		when xabs = 671.72 sync D goto w1611;
	loc w1611: invariant xabs <= 671.8
		when xabs = 671.8 sync C goto w1612;
	loc w1612: invariant xabs <= 671.96
		when xabs = 671.96 sync F goto w1613;
	loc w1613: invariant xabs <= 672
		when xabs = 672 sync E goto w1614;
	loc w1614: invariant xabs <= 672.2
		when xabs = 672.2 sync D goto w1615;
	loc w1615: invariant xabs <= 672.28
		when xabs = 672.28 sync C goto w1616;
	loc w1616: invariant xabs <= 672.44
		when xabs = 672.44 sync F goto w1617;
	loc w1617: invariant xabs <= 672.52
		when xabs = 672.52 sync E goto w1618;
	loc w1618: invariant xabs <= 672.72
		when xabs = 672.72 sync D goto w1619;
	loc w1619: invariant xabs <= 672.8
		when xabs = 672.8 sync C goto w1620;
	loc w1620: invariant xabs <= 672.84
		when xabs = 672.84 sync F goto w1621;
	loc w1621: invariant xabs <= 672.96
		when xabs = 672.96 sync B goto w1622;
	loc w1622: invariant xabs <= 673.08
		when xabs = 673.08 sync C goto w1623;
	loc w1623: invariant xabs <= 673.2
		when xabs = 673.2 sync D goto w1624;
	loc w1624: invariant xabs <= 673.28
		when xabs = 673.28 sync C goto w1625;
	loc w1625: invariant xabs <= 673.4
		when xabs = 673.4 sync F goto w1626;
	loc w1626: invariant xabs <= 673.44
		when xabs = 673.44 sync E goto w1627;
	loc w1627: invariant xabs <= 673.72
		when xabs = 673.72 sync D goto w1628;
	loc w1628: invariant xabs <= 673.76
		when xabs = 673.76 sync C goto w1629;
	loc w1629: invariant xabs <= 673.88
		when xabs = 673.88 sync F goto w1630;
	loc w1630: invariant xabs <= 673.92
		when xabs = 673.92 sync E goto w1631;
	loc w1631: invariant xabs <= 674.2
		when xabs = 674.2 sync D goto w1632;
	loc w1632: invariant xabs <= 674.28
		when xabs = 674.28 sync C goto w1633;
	loc w1633: invariant xabs <= 674.36
		when xabs = 674.36 sync F goto w1634;
	loc w1634: invariant xabs <= 674.44
		when xabs = 674.44 sync E goto w1635;
	loc w1635: invariant xabs <= 674.68
		when xabs = 674.68 sync D goto w1636;
	loc w1636: invariant xabs <= 674.76
		when xabs = 674.76 sync C goto w1637;
	loc w1637: invariant xabs <= 674.88
		when xabs = 674.88 sync F goto w1638;
	loc w1638: invariant xabs <= 674.92
		when xabs = 674.92 sync E goto w1639;
	loc w1639: invariant xabs <= 675.16
		when xabs = 675.16 sync D goto w1640;
	loc w1640: invariant xabs <= 675.24
		when xabs = 675.24 sync C goto w1641;
	loc w1641: invariant xabs <= 675.4
		when xabs = 675.4 sync F goto w1642;
	loc w1642: invariant xabs <= 675.44
		when xabs = 675.44 sync E goto w1643;
	loc w1643: invariant xabs <= 675.64
		when xabs = 675.64 sync D goto w1644;
	loc w1644: invariant xabs <= 675.72
		when xabs = 675.72 sync C goto w1645;
	loc w1645: invariant xabs <= 675.88
		when xabs = 675.88 sync F goto w1646;
	loc w1646: invariant xabs <= 675.92
		when xabs = 675.92 sync E goto w1647;
	loc w1647: invariant xabs <= 676.16
		when xabs = 676.16 sync D goto w1648;
	loc w1648: invariant xabs <= 676.2
		when xabs = 676.2 sync C goto w1649;
	loc w1649: invariant xabs <= 676.36
		when xabs = 676.36 sync F goto w1650;
	loc w1650: invariant xabs <= 676.4
		when xabs = 676.4 sync E goto w1651;
	loc w1651: invariant xabs <= 676.64
		when xabs = 676.64 sync D goto w1652;
	loc w1652: invariant xabs <= 676.72
		when xabs = 676.72 sync C goto w1653;
	loc w1653: invariant xabs <= 676.84
		when xabs = 676.84 sync F goto w1654;
	loc w1654: invariant xabs <= 676.88
		when xabs = 676.88 sync E goto w1655;
	loc w1655: invariant xabs <= 677.16
		when xabs = 677.16 sync D goto w1656;
	loc w1656: invariant xabs <= 677.2
		when xabs = 677.2 sync C goto w1657;
	loc w1657: invariant xabs <= 677.32
		when xabs = 677.32 sync F goto w1658;
	loc w1658: invariant xabs <= 677.36
		when xabs = 677.36 sync E goto w1659;
	loc w1659: invariant xabs <= 677.64
		when xabs = 677.64 sync D goto w1660;
	loc w1660: invariant xabs <= 677.68
		when xabs = 677.68 sync C goto w1661;
	loc w1661: invariant xabs <= 677.8
		when xabs = 677.8 sync F goto w1662;
	loc w1662: invariant xabs <= 677.84
		when xabs = 677.84 sync E goto w1663;
	loc w1663: invariant xabs <= 678.16
		when xabs = 678.16 sync D goto w1664;
	loc w1664: invariant xabs <= 678.28
		when xabs = 678.28 sync C goto w1665;
	loc w1665: invariant xabs <= 678.4
		when xabs = 678.4 sync B goto w1666;
	loc w1666: invariant xabs <= 681.28
		when xabs = 681.28 sync A goto w1667;
	loc w1667: invariant xabs <= 681.56
		when xabs = 681.56 sync B goto w1668;
	loc w1668: invariant xabs <= 681.8
		when xabs = 681.8 sync A goto w1669;
	loc w1669: invariant xabs <= 682.04
		when xabs = 682.04 sync B goto w1670;
	loc w1670: invariant xabs <= 682.12
		when xabs = 682.12 sync A goto w1671;
	loc w1671: invariant xabs <= 682.2
		when xabs = 682.2 sync F goto w1672;
	loc w1672: invariant xabs <= 682.28
		when xabs = 682.28 sync E goto w1673;
	loc w1673: invariant xabs <= 682.52
		when xabs = 682.52 sync B goto w1674;
	loc w1674: invariant xabs <= 682.6
		when xabs = 682.6 sync A goto w1675;
	loc w1675: invariant xabs <= 682.68
		when xabs = 682.68 sync F goto w1676;
	loc w1676: invariant xabs <= 682.72
		when xabs = 682.72 sync E goto w1677;
	loc w1677: invariant xabs <= 683.04
		when xabs = 683.04 sync B goto w1678;
	loc w1678: invariant xabs <= 683.08
		when xabs = 683.08 sync A goto w1679;
	loc w1679: invariant xabs <= 683.16
		when xabs = 683.16 sync F goto w1680;
	loc w1680: invariant xabs <= 683.2
		when xabs = 683.2 sync E goto w1681;
	loc w1681: invariant xabs <= 683.52
		when xabs = 683.52 sync B goto w1682;
	loc w1682: invariant xabs <= 683.6
		when xabs = 683.6 sync A goto w1683;
	loc w1683: invariant xabs <= 683.64
		when xabs = 683.64 sync F goto w1684;
	loc w1684: invariant xabs <= 683.72
		when xabs = 683.72 sync E goto w1685;
	loc w1685: invariant xabs <= 684
		when xabs = 684 sync B goto w1686;
	loc w1686: invariant xabs <= 684.08
		when xabs = 684.08 sync A goto w1687;
	loc w1687: invariant xabs <= 684.16
		when xabs = 684.16 sync F goto w1688;
	loc w1688: invariant xabs <= 684.2
		when xabs = 684.2 sync E goto w1689;
	loc w1689: invariant xabs <= 684.48
		when xabs = 684.48 sync B goto w1690;
	loc w1690: invariant xabs <= 684.56
		when xabs = 684.56 sync A goto w1691;
	loc w1691: invariant xabs <= 684.68
		when xabs = 684.68 sync F goto w1692;
	loc w1692: invariant xabs <= 684.72
		when xabs = 684.72 sync E goto w1693;
	loc w1693: invariant xabs <= 685
		when xabs = 685 sync B goto w1694;
	loc w1694: invariant xabs <= 685.04
		when xabs = 685.04 sync A goto w1695;
	loc w1695: invariant xabs <= 685.16
		when xabs = 685.16 sync F goto w1696;
	loc w1696: invariant xabs <= 685.2
		when xabs = 685.2 sync E goto w1697;
	loc w1697: invariant xabs <= 685.48
		when xabs = 685.48 sync B goto w1698;
	loc w1698: invariant xabs <= 685.56
		when xabs = 685.56 sync A goto w1699;
	loc w1699: invariant xabs <= 685.64
		when xabs = 685.64 sync F goto w1700;
	loc w1700: invariant xabs <= 685.68
		when xabs = 685.68 sync E goto w1701;
	loc w1701: invariant xabs <= 686
		when xabs = 686 sync B goto w1702;
	loc w1702: invariant xabs <= 686.16
		when xabs = 686.16 sync A goto w1703;
	loc w1703: invariant xabs <= 686.48
		when xabs = 686.48 sync B goto w1704;
	loc w1704: invariant xabs <= 686.64
		when xabs = 686.64 sync A goto w1705;
	loc w1705: invariant xabs <= 686.96
		when xabs = 686.96 sync B goto w1706;
	loc w1706: invariant xabs <= 687.04
		when xabs = 687.04 sync A goto w1707;
	loc w1707: invariant xabs <= 687.08
		when xabs = 687.08 sync F goto w1708;
	loc w1708: invariant xabs <= 687.12
		when xabs = 687.12 sync E goto w1709;
	loc w1709: invariant xabs <= 687.44
		when xabs = 687.44 sync B goto w1710;
	loc w1710: invariant xabs <= 687.48
		when xabs = 687.48 sync A goto w1711;
	loc w1711: invariant xabs <= 687.6
		when xabs = 687.6 sync F goto w1712;
	loc w1712: invariant xabs <= 687.64
		when xabs = 687.64 sync E goto w1713;
	loc w1713: invariant xabs <= 687.92
		when xabs = 687.92 sync B goto w1714;
	loc w1714: invariant xabs <= 687.96
		when xabs = 687.96 sync A goto w1715;
	loc w1715: invariant xabs <= 688.08
		when xabs = 688.08 sync F goto w1716;
	loc w1716: invariant xabs <= 688.12
		when xabs = 688.12 sync E goto w1717;
	loc w1717: invariant xabs <= 688.4
		when xabs = 688.4 sync B goto w1718;
	loc w1718: invariant xabs <= 688.48
		when xabs = 688.48 sync A goto w1719;
	loc w1719: invariant xabs <= 688.56
		when xabs = 688.56 sync F goto w1720;
	loc w1720: invariant xabs <= 688.6
		when xabs = 688.6 sync E goto w1721;
	loc w1721: invariant xabs <= 688.92
		when xabs = 688.92 sync B goto w1722;
	loc w1722: invariant xabs <= 688.96
		when xabs = 688.96 sync A goto w1723;
	loc w1723: invariant xabs <= 689.04
		when xabs = 689.04 sync F goto w1724;
	loc w1724: invariant xabs <= 689.08
		when xabs = 689.08 sync E goto w1725;
	loc w1725: invariant xabs <= 689.44
		when xabs = 689.44 sync B goto w1726;
	loc w1726: invariant xabs <= 689.48
		when xabs = 689.48 sync A goto w1727;
	loc w1727: invariant xabs <= 689.52
		when xabs = 689.52 sync F goto w1728;
	loc w1728: invariant xabs <= 689.56
		when xabs = 689.56 sync E goto w1729;
	loc w1729: invariant xabs <= 689.92
		when xabs = 689.92 sync B goto w1730;
	loc w1730: invariant xabs <= 689.96
		when xabs = 689.96 sync A goto w1731;
	loc w1731: invariant xabs <= 690
		when xabs = 690 sync F goto w1732;
	loc w1732: invariant xabs <= 690.08
		when xabs = 690.08 sync E goto w1733;
	loc w1733: invariant xabs <= 690.4
		when xabs = 690.4 sync B goto w1734;
	loc w1734: invariant xabs <= 690.48
		when xabs = 690.48 sync A goto w1735;
	loc w1735: invariant xabs <= 690.52
		when xabs = 690.52 sync F goto w1736;
	loc w1736: invariant xabs <= 690.56
		when xabs = 690.56 sync E goto w1737;
	loc w1737: invariant xabs <= 690.88
		when xabs = 690.88 sync B goto w1738;
	loc w1738: invariant xabs <= 690.96
		when xabs = 690.96 sync A goto w1739;
	loc w1739: invariant xabs <= 691
		when xabs = 691 sync F goto w1740;
	loc w1740: invariant xabs <= 691.08
		when xabs = 691.08 sync E goto w1741;
	loc w1741: invariant xabs <= 691.36
		when xabs = 691.36 sync B goto w1742;
	loc w1742: invariant xabs <= 691.44
		when xabs = 691.44 sync A goto w1743;
	loc w1743: invariant xabs <= 691.48
		when xabs = 691.48 sync F goto w1744;
	loc w1744: invariant xabs <= 691.56
		when xabs = 691.56 sync E goto w1745;
	loc w1745: invariant xabs <= 691.84
		when xabs = 691.84 sync B goto w1746;
	loc w1746: invariant xabs <= 692.04
		when xabs = 692.04 sync A goto w1747;
	loc w1747: invariant xabs <= 692.36
		when xabs = 692.36 sync B goto w1748;
	loc w1748: invariant xabs <= 692.52
		when xabs = 692.52 sync A goto w1749;
	loc w1749: invariant xabs <= 692.84
		when xabs = 692.84 sync B goto w1750;
	loc w1750: invariant xabs <= 693
		when xabs = 693 sync A goto w1751;
	loc w1751: invariant xabs <= 693.32
		when xabs = 693.32 sync B goto w1752;
	loc w1752: invariant xabs <= 693.48
		when xabs = 693.48 sync A goto w1753;
	loc w1753: invariant xabs <= 693.8
		when xabs = 693.8 sync B goto w1754;
	loc w1754: invariant xabs <= 694
		when xabs = 694 sync A goto w1755;
	loc w1755: invariant xabs <= 694.28
		when xabs = 694.28 sync B goto w1756;
	loc w1756: invariant xabs <= 694.36
		when xabs = 694.36 sync A goto w1757;
	loc w1757: invariant xabs <= 694.44
		when xabs = 694.44 sync F goto w1758;
	loc w1758: invariant xabs <= 694.48
		when xabs = 694.48 sync E goto w1759;
	loc w1759: invariant xabs <= 694.8
		when xabs = 694.8 sync B goto w1760;
	loc w1760: invariant xabs <= 694.88
		when xabs = 694.88 sync A goto w1761;
	loc w1761: invariant xabs <= 694.92
		when xabs = 694.92 sync F goto w1762;
	loc w1762: invariant xabs <= 694.96
		when xabs = 694.96 sync E goto w1763;
	loc w1763: invariant xabs <= 695.32
		when xabs = 695.32 sync B goto w1764;
	loc w1764: invariant xabs <= 695.44
		when xabs = 695.44 sync A goto w1765;
	loc w1765: invariant xabs <= 695.8
		when xabs = 695.8 sync B goto w1766;
	loc w1766: invariant xabs <= 695.92
		when xabs = 695.92 sync A goto w1767;
	loc w1767: invariant xabs <= 696.28
		when xabs = 696.28 sync B goto w1768;
	loc w1768: invariant xabs <= 696.4
		when xabs = 696.4 sync A goto w1769;
	loc w1769: invariant xabs <= 696.76
		when xabs = 696.76 sync B goto w1770;
	loc w1770: invariant xabs <= 696.92
		when xabs = 696.92 sync A goto w1771;
	loc w1771: invariant xabs <= 697.24
		when xabs = 697.24 sync B goto w1772;
	loc w1772: invariant xabs <= 697.44
		when xabs = 697.44 sync A goto w1773;
	loc w1773: invariant xabs <= 697.72
		when xabs = 697.72 sync B goto w1774;
	loc w1774: invariant xabs <= 697.92
		when xabs = 697.92 sync A goto w1775;
	loc w1775: invariant xabs <= 698.12
		when xabs = 698.12 sync B goto w1776;
	loc w1776: invariant xabs <= 725.36
		when xabs = 725.36 sync A goto w1777;
	loc w1777: invariant xabs <= 725.64
		when xabs = 725.64 sync B goto w1778;
	loc w1778: invariant xabs <= 725.84
		when xabs = 725.84 sync A goto w1779;
	loc w1779: invariant xabs <= 726.12
		when xabs = 726.12 sync B goto w1780;
	loc w1780: invariant xabs <= 726.32
		when xabs = 726.32 sync A goto w1781;
	loc w1781: invariant xabs <= 726.64
		when xabs = 726.64 sync B goto w1782;
	loc w1782: invariant xabs <= 726.8
		when xabs = 726.8 sync A goto w1783;
	loc w1783: invariant xabs <= 727.12
		when xabs = 727.12 sync B goto w1784;
	loc w1784: invariant xabs <= 727.28
		when xabs = 727.28 sync A goto w1785;
	loc w1785: invariant xabs <= 727.6
		when xabs = 727.6 sync B goto w1786;
	loc w1786: invariant xabs <= 727.76
		when xabs = 727.76 sync A goto w1787;
	loc w1787: invariant xabs <= 728.08
		when xabs = 728.08 sync B goto w1788;
	loc w1788: invariant xabs <= 728.28
		when xabs = 728.28 sync A goto w1789;
	loc w1789: invariant xabs <= 728.56
		when xabs = 728.56 sync B goto w1790;
	loc w1790: invariant xabs <= 728.68
		when xabs = 728.68 sync A goto w1791;
	loc w1791: invariant xabs <= 728.72
		when xabs = 728.72 sync F goto w1792;
	loc w1792: invariant xabs <= 728.8
		when xabs = 728.8 sync E goto w1793;
	loc w1793: invariant xabs <= 729.04
		when xabs = 729.04 sync B goto w1794;
	loc w1794: invariant xabs <= 729.28
		when xabs = 729.28 sync A goto w1795;
	loc w1795: invariant xabs <= 729.56
		when xabs = 729.56 sync B goto w1796;
	loc w1796: invariant xabs <= 729.76
		when xabs = 729.76 sync A goto w1797;
	loc w1797: invariant xabs <= 730.04
		when xabs = 730.04 sync B goto w1798;
	loc w1798: invariant xabs <= 730.24
		when xabs = 730.24 sync A goto w1799;
	loc w1799: invariant xabs <= 730.56
		when xabs = 730.56 sync B goto w1800;
	loc w1800: invariant xabs <= 730.72
		when xabs = 730.72 sync A goto w1801;
	loc w1801: invariant xabs <= 731.04
		when xabs = 731.04 sync B goto w1802;
	loc w1802: invariant xabs <= 731.2
		when xabs = 731.2 sync A goto w1803;
	loc w1803: invariant xabs <= 731.52
		when xabs = 731.52 sync B goto w1804;
	loc w1804: invariant xabs <= 731.6
		when xabs = 731.6 sync A goto w1805;
	loc w1805: invariant xabs <= 731.64
		when xabs = 731.64 sync F goto w1806;
	loc w1806: invariant xabs <= 731.72
		when xabs = 731.72 sync E goto w1807;
	loc w1807: invariant xabs <= 732
		when xabs = 732 sync B goto w1808;
	loc w1808: invariant xabs <= 732.04
		when xabs = 732.04 sync A goto w1809;
	loc w1809: invariant xabs <= 732.16
		when xabs = 732.16 sync F goto w1810;
	loc w1810: invariant xabs <= 732.2
		when xabs = 732.2 sync E goto w1811;
	loc w1811: invariant xabs <= 732.48
		when xabs = 732.48 sync B goto w1812;
	loc w1812: invariant xabs <= 732.52
		when xabs = 732.52 sync A goto w1813;
	loc w1813: invariant xabs <= 732.64
		when xabs = 732.64 sync F goto w1814;
	loc w1814: invariant xabs <= 732.68
		when xabs = 732.68 sync E goto w1815;
	loc w1815: invariant xabs <= 733
		when xabs = 733 sync B goto w1816;
	loc w1816: invariant xabs <= 733.04
		when xabs = 733.04 sync A goto w1817;
	loc w1817: invariant xabs <= 733.12
		when xabs = 733.12 sync F goto w1818;
	loc w1818: invariant xabs <= 733.16
		when xabs = 733.16 sync E goto w1819;
	loc w1819: invariant xabs <= 733.48
		when xabs = 733.48 sync B goto w1820;
	loc w1820: invariant xabs <= 733.52
		when xabs = 733.52 sync A goto w1821;
	loc w1821: invariant xabs <= 733.6
		when xabs = 733.6 sync F goto w1822;
	loc w1822: invariant xabs <= 733.64
		when xabs = 733.64 sync E goto w1823;
	loc w1823: invariant xabs <= 733.96
		when xabs = 733.96 sync B goto w1824;
	loc w1824: invariant xabs <= 734
		when xabs = 734 sync A goto w1825;
	loc w1825: invariant xabs <= 734.12
		when xabs = 734.12 sync F goto w1826;
	loc w1826: invariant xabs <= 734.16
		when xabs = 734.16 sync E goto w1827;
	loc w1827: invariant xabs <= 734.44
		when xabs = 734.44 sync B goto w1828;
	loc w1828: invariant xabs <= 734.48
		when xabs = 734.48 sync A goto w1829;
	loc w1829: invariant xabs <= 734.64
		when xabs = 734.64 sync F goto w1830;
	loc w1830: invariant xabs <= 734.68
		when xabs = 734.68 sync E goto w1831;
	loc w1831: invariant xabs <= 734.92
		when xabs = 734.92 sync B goto w1832;
	loc w1832: invariant xabs <= 734.96
		when xabs = 734.96 sync A goto w1833;
	loc w1833: invariant xabs <= 735.12
		when xabs = 735.12 sync F goto w1834;
	loc w1834: invariant xabs <= 735.16
		when xabs = 735.16 sync E goto w1835;
	loc w1835: invariant xabs <= 735.4
		when xabs = 735.4 sync B goto w1836;
	loc w1836: invariant xabs <= 735.44
		when xabs = 735.44 sync A goto w1837;
	loc w1837: invariant xabs <= 735.6
		when xabs = 735.6 sync F goto w1838;
	loc w1838: invariant xabs <= 735.64
		when xabs = 735.64 sync E goto w1839;
	loc w1839: invariant xabs <= 735.92
		when xabs = 735.92 sync B goto w1840;
	loc w1840: invariant xabs <= 735.96
		when xabs = 735.96 sync A goto w1841;
	loc w1841: invariant xabs <= 736.08
		when xabs = 736.08 sync F goto w1842;
	loc w1842: invariant xabs <= 736.12
		when xabs = 736.12 sync E goto w1843;
	loc w1843: invariant xabs <= 736.4
		when xabs = 736.4 sync B goto w1844;
	loc w1844: invariant xabs <= 736.48
		when xabs = 736.48 sync A goto w1845;
	loc w1845: invariant xabs <= 736.56
		when xabs = 736.56 sync F goto w1846;
	loc w1846: invariant xabs <= 736.6
		when xabs = 736.6 sync E goto w1847;
	loc w1847: invariant xabs <= 736.92
		when xabs = 736.92 sync B goto w1848;
	loc w1848: invariant xabs <= 736.96
		when xabs = 736.96 sync A goto w1849;
	loc w1849: invariant xabs <= 737.04
		when xabs = 737.04 sync F goto w1850;
	loc w1850: invariant xabs <= 737.08
		when xabs = 737.08 sync E goto w1851;
	loc w1851: invariant xabs <= 737.36
		when xabs = 737.36 sync B goto w1852;
	loc w1852: invariant xabs <= 737.44
		when xabs = 737.44 sync A goto w1853;
	loc w1853: invariant xabs <= 737.56
		when xabs = 737.56 sync F goto w1854;
	loc w1854: invariant xabs <= 737.6
		when xabs = 737.6 sync E goto w1855;
	loc w1855: invariant xabs <= 737.84
		when xabs = 737.84 sync B goto w1856;
	loc w1856: invariant xabs <= 737.92
		when xabs = 737.92 sync A goto w1857;
	loc w1857: invariant xabs <= 738
		when xabs = 738 sync F goto w1858;
	loc w1858: invariant xabs <= 738.08
		when xabs = 738.08 sync E goto w1859;
	loc w1859: invariant xabs <= 738.32
		when xabs = 738.32 sync B goto w1860;
	loc w1860: invariant xabs <= 741.6
		when xabs = 741.6 sync A goto w1861;
	loc w1861: invariant xabs <= 741.76
		when xabs = 741.76 sync B goto w1862;
	loc w1862: invariant xabs <= 742.04
		when xabs = 742.04 sync A goto w1863;
	loc w1863: invariant xabs <= 742.24
		when xabs = 742.24 sync B goto w1864;
	loc w1864: invariant xabs <= 742.36
		when xabs = 742.36 sync A goto w1865;
	loc w1865: invariant xabs <= 742.44
		when xabs = 742.44 sync F goto w1866;
	loc w1866: invariant xabs <= 742.52
		when xabs = 742.52 sync E goto w1867;
	loc w1867: invariant xabs <= 742.76
		when xabs = 742.76 sync B goto w1868;
	loc w1868: invariant xabs <= 742.84
		when xabs = 742.84 sync A goto w1869;
	loc w1869: invariant xabs <= 742.92
		when xabs = 742.92 sync F goto w1870;
	loc w1870: invariant xabs <= 743
		when xabs = 743 sync E goto w1871;
	loc w1871: invariant xabs <= 743.24
		when xabs = 743.24 sync B goto w1872;
	loc w1872: invariant xabs <= 743.32
		when xabs = 743.32 sync A goto w1873;
	loc w1873: invariant xabs <= 743.44
		when xabs = 743.44 sync F goto w1874;
	loc w1874: invariant xabs <= 743.48
		when xabs = 743.48 sync E goto w1875;
	loc w1875: invariant xabs <= 743.72
		when xabs = 743.72 sync B goto w1876;
	loc w1876: invariant xabs <= 743.76
		when xabs = 743.76 sync A goto w1877;
	loc w1877: invariant xabs <= 743.96
		when xabs = 743.96 sync F goto w1878;
	loc w1878: invariant xabs <= 744
		when xabs = 744 sync E goto w1879;
	loc w1879: invariant xabs <= 744.2
		when xabs = 744.2 sync B goto w1880;
	loc w1880: invariant xabs <= 744.24
		when xabs = 744.24 sync A goto w1881;
	loc w1881: invariant xabs <= 744.48
		when xabs = 744.48 sync F goto w1882;
	loc w1882: invariant xabs <= 744.76
		when xabs = 744.76 sync B goto w1883;
	loc w1883: invariant xabs <= 744.92
		when xabs = 744.92 sync F goto w1884;
	loc w1884: invariant xabs <= 744.96
		when xabs = 744.96 sync E goto w1885;
	loc w1885: invariant xabs <= 745.16
		when xabs = 745.16 sync C goto w1886;
	loc w1886: invariant xabs <= 745.24
		when xabs = 745.24 sync B goto w1887;
	loc w1887: invariant xabs <= 745.4
		when xabs = 745.4 sync F goto w1888;
	loc w1888: invariant xabs <= 745.44
		when xabs = 745.44 sync E goto w1889;
	loc w1889: invariant xabs <= 745.68
		when xabs = 745.68 sync C goto w1890;
	loc w1890: invariant xabs <= 745.76
		when xabs = 745.76 sync B goto w1891;
	loc w1891: invariant xabs <= 745.88
		when xabs = 745.88 sync F goto w1892;
	loc w1892: invariant xabs <= 745.92
		when xabs = 745.92 sync E goto w1893;
	loc w1893: invariant xabs <= 746.16
		when xabs = 746.16 sync C goto w1894;
	loc w1894: invariant xabs <= 746.24
		when xabs = 746.24 sync B goto w1895;
	loc w1895: invariant xabs <= 746.36
		when xabs = 746.36 sync F goto w1896;
	loc w1896: invariant xabs <= 746.4
		when xabs = 746.4 sync E goto w1897;
	loc w1897: invariant xabs <= 746.64
		when xabs = 746.64 sync C goto w1898;
	loc w1898: invariant xabs <= 746.72
		when xabs = 746.72 sync B goto w1899;
	loc w1899: invariant xabs <= 746.88
		when xabs = 746.88 sync F goto w1900;
	loc w1900: invariant xabs <= 746.92
		when xabs = 746.92 sync E goto w1901;
	loc w1901: invariant xabs <= 747.12
		when xabs = 747.12 sync C goto w1902;
	loc w1902: invariant xabs <= 747.2
		when xabs = 747.2 sync B goto w1903;
	loc w1903: invariant xabs <= 747.4
		when xabs = 747.4 sync F goto w1904;
	loc w1904: invariant xabs <= 747.44
		when xabs = 747.44 sync E goto w1905;
	loc w1905: invariant xabs <= 747.6
		when xabs = 747.6 sync C goto w1906;
	loc w1906: invariant xabs <= 747.68
		when xabs = 747.68 sync B goto w1907;
	loc w1907: invariant xabs <= 747.88
		when xabs = 747.88 sync F goto w1908;
	loc w1908: invariant xabs <= 747.92
		when xabs = 747.92 sync E goto w1909;
	loc w1909: invariant xabs <= 748.12
		when xabs = 748.12 sync C goto w1910;
	loc w1910: invariant xabs <= 748.16
		when xabs = 748.16 sync B goto w1911;
	loc w1911: invariant xabs <= 748.36
		when xabs = 748.36 sync F goto w1912;
	loc w1912: invariant xabs <= 748.4
		when xabs = 748.4 sync E goto w1913;
	loc w1913: invariant xabs <= 748.6
		when xabs = 748.6 sync C goto w1914;
	loc w1914: invariant xabs <= 748.68
		when xabs = 748.68 sync B goto w1915;
	loc w1915: invariant xabs <= 748.84
		when xabs = 748.84 sync F goto w1916;
	loc w1916: invariant xabs <= 748.88
		when xabs = 748.88 sync E goto w1917;
	loc w1917: invariant xabs <= 749.12
		when xabs = 749.12 sync C goto w1918;
	loc w1918: invariant xabs <= 749.16
		when xabs = 749.16 sync B goto w1919;
	loc w1919: invariant xabs <= 749.32
		when xabs = 749.32 sync F goto w1920;
	loc w1920: invariant xabs <= 749.36
		when xabs = 749.36 sync E goto w1921;
	loc w1921: invariant xabs <= 749.6
		when xabs = 749.6 sync C goto w1922;
	loc w1922: invariant xabs <= 749.64
		when xabs = 749.64 sync B goto w1923;
	loc w1923: invariant xabs <= 749.84
		when xabs = 749.84 sync F goto w1924;
	loc w1924: invariant xabs <= 750.08
		when xabs = 750.08 sync C goto w1925;
	loc w1925: invariant xabs <= 750.12
		when xabs = 750.12 sync B goto w1926;
	loc w1926: invariant xabs <= 750.36
		when xabs = 750.36 sync F goto w1927;
	loc w1927: invariant xabs <= 750.56
		when xabs = 750.56 sync C goto w1928;
	loc w1928: invariant xabs <= 750.6
		when xabs = 750.6 sync B goto w1929;
	loc w1929: invariant xabs <= 750.84
		when xabs = 750.84 sync F goto w1930;
	loc w1930: invariant xabs <= 750.88
		when xabs = 750.88 sync E goto w1931;
	loc w1931: invariant xabs <= 751.08
		when xabs = 751.08 sync C goto w1932;
	loc w1932: invariant xabs <= 751.32
		when xabs = 751.32 sync F goto w1933;
	loc w1933: invariant xabs <= 751.36
		when xabs = 751.36 sync E goto w1934;
	loc w1934: invariant xabs <= 751.52
		when xabs = 751.52 sync D goto w1935;
	loc w1935: invariant xabs <= 751.56
		when xabs = 751.56 sync C goto w1936;
	loc w1936: invariant xabs <= 751.8
		when xabs = 751.8 sync F goto w1937;
	loc w1937: invariant xabs <= 751.84
		when xabs = 751.84 sync E goto w1938;
	loc w1938: invariant xabs <= 752.04
		when xabs = 752.04 sync D goto w1939;
	loc w1939: invariant xabs <= 752.08
		when xabs = 752.08 sync C goto w1940;
	loc w1940: invariant xabs <= 752.28
		when xabs = 752.28 sync F goto w1941;
	loc w1941: invariant xabs <= 752.32
		when xabs = 752.32 sync E goto w1942;
	loc w1942: invariant xabs <= 752.52
		when xabs = 752.52 sync D goto w1943;
	loc w1943: invariant xabs <= 752.56
		when xabs = 752.56 sync C goto w1944;
	loc w1944: invariant xabs <= 752.76
		when xabs = 752.76 sync F goto w1945;
	loc w1945: invariant xabs <= 752.8
		when xabs = 752.8 sync E goto w1946;
	loc w1946: invariant xabs <= 753
		when xabs = 753 sync D goto w1947;
	loc w1947: invariant xabs <= 753.08
		when xabs = 753.08 sync C goto w1948;
	loc w1948: invariant xabs <= 753.28
		when xabs = 753.28 sync F goto w1949;
	loc w1949: invariant xabs <= 753.32
		when xabs = 753.32 sync E goto w1950;
	loc w1950: invariant xabs <= 753.48
		when xabs = 753.48 sync D goto w1951;
	loc w1951: invariant xabs <= 753.52
		when xabs = 753.52 sync C goto w1952;
	loc w1952: invariant xabs <= 753.76
		when xabs = 753.76 sync F goto w1953;
	loc w1953: invariant xabs <= 753.84
		when xabs = 753.84 sync E goto w1954;
	loc w1954: invariant xabs <= 753.96
		when xabs = 753.96 sync D goto w1955;
	loc w1955: invariant xabs <= 754
		when xabs = 754 sync C goto w1956;
	loc w1956: invariant xabs <= 754.28
		when xabs = 754.28 sync F goto w1957;
	loc w1957: invariant xabs <= 754.32
		when xabs = 754.32 sync E goto w1958;
	loc w1958: invariant xabs <= 754.44
		when xabs = 754.44 sync D goto w1959;
	loc w1959: invariant xabs <= 754.48
		when xabs = 754.48 sync C goto w1960;
	loc w1960: invariant xabs <= 754.76
		when xabs = 754.76 sync F goto w1961;
	loc w1961: invariant xabs <= 754.8
		when xabs = 754.8 sync E goto w1962;
	loc w1962: invariant xabs <= 754.96
		when xabs = 754.96 sync D goto w1963;
	loc w1963: invariant xabs <= 755
		when xabs = 755 sync C goto w1964;
	loc w1964: invariant xabs <= 755.2
		when xabs = 755.2 sync F goto w1965;
	loc w1965: invariant xabs <= 755.24
		when xabs = 755.24 sync E goto w1966;
	loc w1966: invariant xabs <= 755.44
		when xabs = 755.44 sync D goto w1967;
	loc w1967: invariant xabs <= 755.52
		when xabs = 755.52 sync C goto w1968;
	loc w1968: invariant xabs <= 755.68
		when xabs = 755.68 sync F goto w1969;
	loc w1969: invariant xabs <= 755.76
		when xabs = 755.76 sync E goto w1970;
	loc w1970: invariant xabs <= 755.92
		when xabs = 755.92 sync D goto w1971;
	loc w1971: invariant xabs <= 756
		when xabs = 756 sync C goto w1972;
	loc w1972: invariant xabs <= 756.2
		when xabs = 756.2 sync F goto w1973;
	loc w1973: invariant xabs <= 756.24
		when xabs = 756.24 sync E goto w1974;
	loc w1974: invariant xabs <= 756.4
		when xabs = 756.4 sync D goto w1975;
	loc w1975: invariant xabs <= 756.48
		when xabs = 756.48 sync C goto w1976;
	loc w1976: invariant xabs <= 756.76
		when xabs = 756.76 sync F goto w1977;
	loc w1977: invariant xabs <= 756.88
		when xabs = 756.88 sync D goto w1978;
	loc w1978: invariant xabs <= 756.92
		when xabs = 756.92 sync C goto w1979;
	loc w1979: invariant xabs <= 757.24
		when xabs = 757.24 sync F goto w1980;
	loc w1980: invariant xabs <= 757.28
		when xabs = 757.28 sync D goto w1981;
	loc w1981: invariant xabs <= 757.32
		when xabs = 757.32 sync E goto w1982;
	loc w1982: invariant xabs <= 757.36
		when xabs = 757.36 sync F goto w1983;
	loc w1983: invariant xabs <= 757.72
		when xabs = 757.72 sync C goto w1984;
	loc w1984: invariant xabs <= 757.88
		when xabs = 757.88 sync D goto w1985;
	loc w1985: invariant xabs <= 758
		when xabs = 758 sync C goto w1986;
	loc w1986: invariant xabs <= 758.2
		when xabs = 758.2 sync E goto w1987;
	loc w1987: invariant xabs <= 758.32
		when xabs = 758.32 sync B goto w1988;
	loc w1988: invariant xabs <= 760.96
		when xabs = 760.96 sync A goto w1989;
	loc w1989: invariant xabs <= 761.12
		when xabs = 761.12 sync F goto w1990;
	loc w1990: invariant xabs <= 761.16
		when xabs = 761.16 sync E goto w1991;
	loc w1991: invariant xabs <= 761.28
		when xabs = 761.28 sync B goto w1992;
	loc w1992: invariant xabs <= 761.44
		when xabs = 761.44 sync A goto w1993;
	loc w1993: invariant xabs <= 761.6
		when xabs = 761.6 sync F goto w1994;
	loc w1994: invariant xabs <= 761.64
		when xabs = 761.64 sync E goto w1995;
	loc w1995: invariant xabs <= 761.8
		when xabs = 761.8 sync B goto w1996;
	loc w1996: invariant xabs <= 761.88
		when xabs = 761.88 sync A goto w1997;
	loc w1997: invariant xabs <= 762.08
		when xabs = 762.08 sync F goto w1998;
	loc w1998: invariant xabs <= 762.12
		when xabs = 762.12 sync E goto w1999;
	loc w1999: invariant xabs <= 762.28
		when xabs = 762.28 sync B goto w2000;
	loc w2000: invariant xabs <= 762.36
		when xabs = 762.36 sync A goto w2001;
	loc w2001: invariant xabs <= 762.64
		when xabs = 762.64 sync F goto w2002;
	loc w2002: invariant xabs <= 762.72
		when xabs = 762.72 sync B goto w2003;
	loc w2003: invariant xabs <= 762.76
		when xabs = 762.76 sync F goto w2004;
	loc w2004: invariant xabs <= 763.32
		when xabs = 763.32 sync A goto w2005;
	loc w2005: invariant xabs <= 764.6
		when xabs = 764.6 sync B goto w2006;
	loc w2006: invariant xabs <= 765.04
		when xabs = 765.04 sync C goto w2007;
	loc w2007: invariant xabs <= 765.08
		when xabs = 765.08 sync E goto w2008;
	loc w2008: invariant xabs <= 765.2
		when xabs = 765.2 sync D goto w2009;
	loc w2009: invariant xabs <= 765.28
		when xabs = 765.28 sync C goto w2010;
	loc w2010: invariant xabs <= 767.56
		when xabs = 767.56 sync F goto w2011;
	loc w2011: invariant xabs <= 767.68
		when xabs = 767.68 sync D goto w2012;
	loc w2012: invariant xabs <= 768.04
		when xabs = 768.04 sync C goto w2013;
	loc w2013: invariant xabs <= 768.48
		when xabs = 768.48 sync D goto w2014;
	loc w2014: invariant xabs <= 768.56
		when xabs = 768.56 sync E goto w2015;
	loc w2015: invariant xabs <= 770.36
		when xabs = 770.36 sync F goto w2016;
	loc w2016: invariant xabs <= 778
		when xabs = 778 sync H goto w2017;
	loc w2017: invariant xabs <= 778.08
		when xabs = 778.08 sync E goto w2018;
	loc w2018: invariant xabs <= 778.28
		when xabs = 778.28 sync G goto w2019;
	loc w2019: invariant xabs <= 778.4
		when xabs = 778.4 sync C goto w2020;
	loc w2020: invariant xabs <= 778.52
		when xabs = 778.52 sync B goto w2021;
	loc w2021: invariant xabs <= 780.4
		when xabs = 780.4 sync A goto w2022;
	loc w2022: invariant xabs <= 781.48
		when xabs = 781.48 sync F goto w2023;
	loc w2023: invariant xabs <= 782.88
		when xabs = 782.88 sync B goto w2024;
	loc w2024: invariant xabs <= 786.2
		when xabs = 786.2 sync C goto w2025;
	loc w2025: invariant xabs <= 786.28
		when xabs = 786.28 sync H goto w2026;
	loc w2026: invariant xabs <= 798
		when xabs = 798 sync D goto w2027;
	loc w2027: invariant xabs <= 798.12
		when xabs = 798.12 sync E goto w2028;
	loc w2028: invariant xabs <= 798.32
		when xabs = 798.32 sync G goto w2029;
	loc w2029: invariant xabs <= 798.44
		when xabs = 798.44 sync C goto w2030;
	loc w2030: invariant xabs <= 798.64
		when xabs = 798.64 sync B goto w2031;
	loc w2031: invariant xabs <= 800.36
		when xabs = 800.36 sync A goto w2032;
	loc w2032: invariant xabs <= 801.08
		when xabs = 801.08 sync F goto w2033;
	loc w2033: invariant xabs <= 802.24
		when xabs = 802.24 sync B goto w2034;
	loc w2034: invariant xabs <= 804.76
		when xabs = 804.76 sync C goto w2035;
	loc w2035: invariant xabs <= 804.84
		when xabs = 804.84 sync H goto w2036;
	loc w2036: invariant xabs <= 818
		when xabs = 818 sync D goto w2037;
	loc w2037: invariant xabs <= 818.12
		when xabs = 818.12 sync E goto w2038;
	loc w2038: invariant xabs <= 818.32
		when xabs = 818.32 sync G goto w2039;
	loc w2039: invariant xabs <= 818.44
		when xabs = 818.44 sync C goto w2040;
	loc w2040: invariant xabs <= 818.56
		when xabs = 818.56 sync B goto w2041;
	loc w2041: invariant xabs <= 820.44
		when xabs = 820.44 sync A goto w2042;
	loc w2042: invariant xabs <= 821.32
		when xabs = 821.32 sync F goto w2043;
	loc w2043: invariant xabs <= 823.36
		when xabs = 823.36 sync B goto w2044;
	loc w2044: invariant xabs <= 826.48
		when xabs = 826.48 sync C goto w2045;
	loc w2045: invariant xabs <= 826.56
		when xabs = 826.56 sync H goto w2046;
	loc w2046: invariant xabs <= 837.08
		when xabs = 837.08 sync D goto w2047;
	loc w2047: invariant xabs <= 837.12
		when xabs = 837.12 sync E goto w2048;
	loc w2048: invariant xabs <= 837.56
		when xabs = 837.56 sync F goto w2049;
	loc w2049: invariant xabs <= 837.64
		when xabs = 837.64 sync E goto w2050;
	loc w2050: invariant xabs <= 838
		when xabs = 838 sync F goto w2051;
	loc w2051: invariant xabs <= 838.08
		when xabs = 838.08 sync E goto w2052;
	loc w2052: invariant xabs <= 838.28
		when xabs = 838.28 sync G goto w2053;
	loc w2053: invariant xabs <= 838.4
		when xabs = 838.4 sync C goto w2054;
	loc w2054: invariant xabs <= 838.56
		when xabs = 838.56 sync B goto w2055;
	loc w2055: invariant xabs <= 840.96
		when xabs = 840.96 sync A goto w2056;
	loc w2056: invariant xabs <= 841.12
		when xabs = 841.12 sync B goto w2057;
	loc w2057: invariant xabs <= 841.28
		when xabs = 841.28 sync A goto w2058;
	loc w2058: invariant xabs <= 841.44
		when xabs = 841.44 sync F goto w2059;
	loc w2059: invariant xabs <= 841.64
		when xabs = 841.64 sync E goto w2060;
	loc w2060: invariant xabs <= 842.44
		when xabs = 842.44 sync F goto w2061;
	loc w2061: invariant xabs <= 842.88
		when xabs = 842.88 sync B goto w2062;
	loc w2062: invariant xabs <= 842.92
		when xabs = 842.92 sync E goto w2063;
	loc w2063: invariant xabs <= 843.08
		when xabs = 843.08 sync C goto w2064;
	loc w2064: invariant xabs <= 843.16
		when xabs = 843.16 sync B goto w2065;
	loc w2065: invariant xabs <= 843.36
		when xabs = 843.36 sync F goto w2066;
	loc w2066: invariant xabs <= 843.4
		when xabs = 843.4 sync E goto w2067;
	loc w2067: invariant xabs <= 843.6
		when xabs = 843.6 sync C goto w2068;
	loc w2068: invariant xabs <= 843.64
		when xabs = 843.64 sync B goto w2069;
	loc w2069: invariant xabs <= 843.88
		when xabs = 843.88 sync F goto w2070;
	loc w2070: invariant xabs <= 844.08
		when xabs = 844.08 sync C goto w2071;
	loc w2071: invariant xabs <= 844.12
		when xabs = 844.12 sync B goto w2072;
	loc w2072: invariant xabs <= 844.36
		when xabs = 844.36 sync F goto w2073;
	loc w2073: invariant xabs <= 844.4
		when xabs = 844.4 sync E goto w2074;
	loc w2074: invariant xabs <= 844.56
		when xabs = 844.56 sync C goto w2075;
	loc w2075: invariant xabs <= 844.6
		when xabs = 844.6 sync B goto w2076;
	loc w2076: invariant xabs <= 845.4
		when xabs = 845.4 sync F goto w2077;
	loc w2077: invariant xabs <= 845.84
		when xabs = 845.84 sync C goto w2078;
	loc w2078: invariant xabs <= 846
		when xabs = 846 sync D goto w2079;
	loc w2079: invariant xabs <= 846.08
		when xabs = 846.08 sync C goto w2080;
	loc w2080: invariant xabs <= 846.28
		when xabs = 846.28 sync F goto w2081;
	loc w2081: invariant xabs <= 846.32
		when xabs = 846.32 sync E goto w2082;
	loc w2082: invariant xabs <= 846.52
		when xabs = 846.52 sync D goto w2083;
	loc w2083: invariant xabs <= 846.6
		when xabs = 846.6 sync C goto w2084;
	loc w2084: invariant xabs <= 846.76
		when xabs = 846.76 sync F goto w2085;
	loc w2085: invariant xabs <= 846.84
		when xabs = 846.84 sync E goto w2086;
	loc w2086: invariant xabs <= 847
		when xabs = 847 sync D goto w2087;
	loc w2087: invariant xabs <= 847.08
		when xabs = 847.08 sync C goto w2088;
	loc w2088: invariant xabs <= 847.28
		when xabs = 847.28 sync F goto w2089;
	loc w2089: invariant xabs <= 847.32
		when xabs = 847.32 sync E goto w2090;
	loc w2090: invariant xabs <= 847.48
		when xabs = 847.48 sync D goto w2091;
	loc w2091: invariant xabs <= 847.56
		when xabs = 847.56 sync C goto w2092;
	loc w2092: invariant xabs <= 847.8
		when xabs = 847.8 sync F goto w2093;
	loc w2093: invariant xabs <= 847.84
		when xabs = 847.84 sync E goto w2094;
	loc w2094: invariant xabs <= 847.96
		when xabs = 847.96 sync D goto w2095;
	loc w2095: invariant xabs <= 848.04
		when xabs = 848.04 sync C goto w2096;
	loc w2096: invariant xabs <= 848.28
		when xabs = 848.28 sync F goto w2097;
	loc w2097: invariant xabs <= 848.32
		when xabs = 848.32 sync E goto w2098;
	loc w2098: invariant xabs <= 848.48
		when xabs = 848.48 sync D goto w2099;
	loc w2099: invariant xabs <= 848.52
		when xabs = 848.52 sync C goto w2100;
	loc w2100: invariant xabs <= 848.76
		when xabs = 848.76 sync F goto w2101;
	loc w2101: invariant xabs <= 848.8
		when xabs = 848.8 sync E goto w2102;
	loc w2102: invariant xabs <= 848.96
		when xabs = 848.96 sync D goto w2103;
	loc w2103: invariant xabs <= 849.04
		when xabs = 849.04 sync C goto w2104;
	loc w2104: invariant xabs <= 849.24
		when xabs = 849.24 sync F goto w2105;
	loc w2105: invariant xabs <= 849.28
		when xabs = 849.28 sync E goto w2106;
	loc w2106: invariant xabs <= 849.48
		when xabs = 849.48 sync D goto w2107;
	loc w2107: invariant xabs <= 849.52
		when xabs = 849.52 sync C goto w2108;
	loc w2108: invariant xabs <= 849.72
		when xabs = 849.72 sync F goto w2109;
	loc w2109: invariant xabs <= 849.76
		when xabs = 849.76 sync E goto w2110;
	loc w2110: invariant xabs <= 849.96
		when xabs = 849.96 sync D goto w2111;
	loc w2111: invariant xabs <= 850.04
		when xabs = 850.04 sync C goto w2112;
	loc w2112: invariant xabs <= 850.2
		when xabs = 850.2 sync F goto w2113;
	loc w2113: invariant xabs <= 850.24
		when xabs = 850.24 sync E goto w2114;
	loc w2114: invariant xabs <= 850.44
		when xabs = 850.44 sync D goto w2115;
	loc w2115: invariant xabs <= 850.52
		when xabs = 850.52 sync C goto w2116;
	loc w2116: invariant xabs <= 850.72
		when xabs = 850.72 sync F goto w2117;
	loc w2117: invariant xabs <= 850.76
		when xabs = 850.76 sync E goto w2118;
	loc w2118: invariant xabs <= 850.92
		when xabs = 850.92 sync D goto w2119;
	loc w2119: invariant xabs <= 850.96
		when xabs = 850.96 sync C goto w2120;
	loc w2120: invariant xabs <= 851.24
		when xabs = 851.24 sync F goto w2121;
	loc w2121: invariant xabs <= 851.4
		when xabs = 851.4 sync D goto w2122;
	loc w2122: invariant xabs <= 851.44
		when xabs = 851.44 sync C goto w2123;
	loc w2123: invariant xabs <= 851.72
		when xabs = 851.72 sync F goto w2124;
	loc w2124: invariant xabs <= 851.92
		when xabs = 851.92 sync D goto w2125;
	loc w2125: invariant xabs <= 851.96
		when xabs = 851.96 sync C goto w2126;
	loc w2126: invariant xabs <= 852.16
		when xabs = 852.16 sync F goto w2127;
	loc w2127: invariant xabs <= 852.2
		when xabs = 852.2 sync E goto w2128;
	loc w2128: invariant xabs <= 852.4
		when xabs = 852.4 sync D goto w2129;
	loc w2129: invariant xabs <= 852.48
		when xabs = 852.48 sync C goto w2130;
	loc w2130: invariant xabs <= 852.64
		when xabs = 852.64 sync F goto w2131;
	loc w2131: invariant xabs <= 852.68
		when xabs = 852.68 sync E goto w2132;
	loc w2132: invariant xabs <= 852.92
		when xabs = 852.92 sync D goto w2133;
	loc w2133: invariant xabs <= 852.96
		when xabs = 852.96 sync C goto w2134;
	loc w2134: invariant xabs <= 853.16
		when xabs = 853.16 sync F goto w2135;
	loc w2135: invariant xabs <= 853.4
		when xabs = 853.4 sync D goto w2136;
	loc w2136: invariant xabs <= 853.44
		when xabs = 853.44 sync C goto w2137;
	loc w2137: invariant xabs <= 853.64
		when xabs = 853.64 sync F goto w2138;
	loc w2138: invariant xabs <= 853.68
		when xabs = 853.68 sync E goto w2139;
	loc w2139: invariant xabs <= 853.88
		when xabs = 853.88 sync D goto w2140;
	loc w2140: invariant xabs <= 853.92
		when xabs = 853.92 sync C goto w2141;
	loc w2141: invariant xabs <= 854.16
		when xabs = 854.16 sync F goto w2142;
	loc w2142: invariant xabs <= 854.36
		when xabs = 854.36 sync D goto w2143;
	loc w2143: invariant xabs <= 854.4
		when xabs = 854.4 sync C goto w2144;
	loc w2144: invariant xabs <= 854.64
		when xabs = 854.64 sync F goto w2145;
	loc w2145: invariant xabs <= 854.68
		when xabs = 854.68 sync E goto w2146;
	loc w2146: invariant xabs <= 854.84
		when xabs = 854.84 sync D goto w2147;
	loc w2147: invariant xabs <= 854.88
		when xabs = 854.88 sync C goto w2148;
	loc w2148: invariant xabs <= 855.12
		when xabs = 855.12 sync F goto w2149;
	loc w2149: invariant xabs <= 855.16
		when xabs = 855.16 sync E goto w2150;
	loc w2150: invariant xabs <= 855.36
		when xabs = 855.36 sync D goto w2151;
	loc w2151: invariant xabs <= 855.4
		when xabs = 855.4 sync C goto w2152;
	loc w2152: invariant xabs <= 855.6
		when xabs = 855.6 sync F goto w2153;
	loc w2153: invariant xabs <= 855.84
		when xabs = 855.84 sync D goto w2154;
	loc w2154: invariant xabs <= 855.92
		when xabs = 855.92 sync C goto w2155;
	loc w2155: invariant xabs <= 856.08
		when xabs = 856.08 sync F goto w2156;
	loc w2156: invariant xabs <= 856.36
		when xabs = 856.36 sync D goto w2157;
	loc w2157: invariant xabs <= 856.4
		when xabs = 856.4 sync C goto w2158;
	loc w2158: invariant xabs <= 856.56
		when xabs = 856.56 sync F goto w2159;
	loc w2159: invariant xabs <= 856.6
		when xabs = 856.6 sync E goto w2160;
	loc w2160: invariant xabs <= 856.84
		when xabs = 856.84 sync D goto w2161;
	loc w2161: invariant xabs <= 856.88
		when xabs = 856.88 sync C goto w2162;
	loc w2162: invariant xabs <= 857.08
		when xabs = 857.08 sync F goto w2163;
	loc w2163: invariant xabs <= 857.32
		when xabs = 857.32 sync D goto w2164;
	loc w2164: invariant xabs <= 857.36
		when xabs = 857.36 sync C goto w2165;
	loc w2165: invariant xabs <= 857.56
		when xabs = 857.56 sync F goto w2166;
	loc w2166: invariant xabs <= 857.6
		when xabs = 857.6 sync E goto w2167;
	loc w2167: invariant xabs <= 857.8
		when xabs = 857.8 sync D goto w2168;
	loc w2168: invariant xabs <= 857.84
		when xabs = 857.84 sync C goto w2169;
	loc w2169: invariant xabs <= 858
		when xabs = 858 sync F goto w2170;
	loc w2170: invariant xabs <= 858.2
		when xabs = 858.2 sync E goto w2171;
	loc w2171: invariant xabs <= 858.32
		when xabs = 858.32 sync B goto w2172;
	loc w2172: invariant xabs <= 861.48
		when xabs = 861.48 sync A goto w2173;
	loc w2173: invariant xabs <= 861.72
		when xabs = 861.72 sync B goto w2174;
	loc w2174: invariant xabs <= 861.96
		when xabs = 861.96 sync A goto w2175;
	loc w2175: invariant xabs <= 862.24
		when xabs = 862.24 sync B goto w2176;
	loc w2176: invariant xabs <= 862.44
		when xabs = 862.44 sync A goto w2177;
	loc w2177: invariant xabs <= 862.72
		when xabs = 862.72 sync B goto w2178;
	loc w2178: invariant xabs <= 862.96
		when xabs = 862.96 sync A goto w2179;
	loc w2179: invariant xabs <= 863.2
		when xabs = 863.2 sync B goto w2180;
	loc w2180: invariant xabs <= 863.44
		when xabs = 863.44 sync A goto w2181;
	loc w2181: invariant xabs <= 863.68
		when xabs = 863.68 sync B goto w2182;
	loc w2182: invariant xabs <= 863.8
		when xabs = 863.8 sync A goto w2183;
	loc w2183: invariant xabs <= 863.88
		when xabs = 863.88 sync F goto w2184;
	loc w2184: invariant xabs <= 863.96
		when xabs = 863.96 sync E goto w2185;
	loc w2185: invariant xabs <= 864.16
		when xabs = 864.16 sync B goto w2186;
	loc w2186: invariant xabs <= 864.24
		when xabs = 864.24 sync A goto w2187;
	loc w2187: invariant xabs <= 864.36
		when xabs = 864.36 sync F goto w2188;
	loc w2188: invariant xabs <= 864.44
		when xabs = 864.44 sync E goto w2189;
	loc w2189: invariant xabs <= 864.68
		when xabs = 864.68 sync B goto w2190;
	loc w2190: invariant xabs <= 864.72
		when xabs = 864.72 sync A goto w2191;
	loc w2191: invariant xabs <= 864.88
		when xabs = 864.88 sync F goto w2192;
	loc w2192: invariant xabs <= 864.92
		when xabs = 864.92 sync E goto w2193;
	loc w2193: invariant xabs <= 865.2
		when xabs = 865.2 sync B goto w2194;
	loc w2194: invariant xabs <= 865.24
		when xabs = 865.24 sync A goto w2195;
	loc w2195: invariant xabs <= 865.36
		when xabs = 865.36 sync F goto w2196;
	loc w2196: invariant xabs <= 865.4
		when xabs = 865.4 sync E goto w2197;
	loc w2197: invariant xabs <= 865.68
		when xabs = 865.68 sync B goto w2198;
	loc w2198: invariant xabs <= 865.72
		when xabs = 865.72 sync A goto w2199;
	loc w2199: invariant xabs <= 865.84
		when xabs = 865.84 sync F goto w2200;
	loc w2200: invariant xabs <= 865.88
		when xabs = 865.88 sync E goto w2201;
	loc w2201: invariant xabs <= 866.16
		when xabs = 866.16 sync B goto w2202;
	loc w2202: invariant xabs <= 866.2
		when xabs = 866.2 sync A goto w2203;
	loc w2203: invariant xabs <= 866.32
		when xabs = 866.32 sync F goto w2204;
	loc w2204: invariant xabs <= 866.36
		when xabs = 866.36 sync E goto w2205;
	loc w2205: invariant xabs <= 866.64
		when xabs = 866.64 sync B goto w2206;
	loc w2206: invariant xabs <= 866.68
		when xabs = 866.68 sync A goto w2207;
	loc w2207: invariant xabs <= 866.84
		when xabs = 866.84 sync F goto w2208;
	loc w2208: invariant xabs <= 866.88
		when xabs = 866.88 sync E goto w2209;
	loc w2209: invariant xabs <= 867.12
		when xabs = 867.12 sync B goto w2210;
	loc w2210: invariant xabs <= 867.16
		when xabs = 867.16 sync A goto w2211;
	loc w2211: invariant xabs <= 867.32
		when xabs = 867.32 sync F goto w2212;
	loc w2212: invariant xabs <= 867.36
		when xabs = 867.36 sync E goto w2213;
	loc w2213: invariant xabs <= 867.6
		when xabs = 867.6 sync B goto w2214;
	loc w2214: invariant xabs <= 867.68
		when xabs = 867.68 sync A goto w2215;
	loc w2215: invariant xabs <= 867.8
		when xabs = 867.8 sync F goto w2216;
	loc w2216: invariant xabs <= 867.84
		when xabs = 867.84 sync E goto w2217;
	loc w2217: invariant xabs <= 868.12
		when xabs = 868.12 sync B goto w2218;
	loc w2218: invariant xabs <= 868.16
		when xabs = 868.16 sync A goto w2219;
	loc w2219: invariant xabs <= 868.28
		when xabs = 868.28 sync F goto w2220;
	loc w2220: invariant xabs <= 868.32
		when xabs = 868.32 sync E goto w2221;
	loc w2221: invariant xabs <= 868.64
		when xabs = 868.64 sync B goto w2222;
	loc w2222: invariant xabs <= 868.68
		when xabs = 868.68 sync A goto w2223;
	loc w2223: invariant xabs <= 868.76
		when xabs = 868.76 sync F goto w2224;
	loc w2224: invariant xabs <= 868.8
		when xabs = 868.8 sync E goto w2225;
	loc w2225: invariant xabs <= 869.12
		when xabs = 869.12 sync B goto w2226;
	loc w2226: invariant xabs <= 869.16
		when xabs = 869.16 sync A goto w2227;
	loc w2227: invariant xabs <= 869.24
		when xabs = 869.24 sync F goto w2228;
	loc w2228: invariant xabs <= 869.28
		when xabs = 869.28 sync E goto w2229;
	loc w2229: invariant xabs <= 869.6
		when xabs = 869.6 sync B goto w2230;
	loc w2230: invariant xabs <= 869.64
		when xabs = 869.64 sync A goto w2231;
	loc w2231: invariant xabs <= 869.76
		when xabs = 869.76 sync F goto w2232;
	loc w2232: invariant xabs <= 869.8
		when xabs = 869.8 sync E goto w2233;
	loc w2233: invariant xabs <= 870.08
		when xabs = 870.08 sync B goto w2234;
	loc w2234: invariant xabs <= 870.12
		when xabs = 870.12 sync A goto w2235;
	loc w2235: invariant xabs <= 870.28
		when xabs = 870.28 sync F goto w2236;
	loc w2236: invariant xabs <= 870.56
		when xabs = 870.56 sync B goto w2237;
	loc w2237: invariant xabs <= 870.6
		when xabs = 870.6 sync A goto w2238;
	loc w2238: invariant xabs <= 870.76
		when xabs = 870.76 sync F goto w2239;
	loc w2239: invariant xabs <= 871.04
		when xabs = 871.04 sync B goto w2240;
	loc w2240: invariant xabs <= 871.12
		when xabs = 871.12 sync A goto w2241;
	loc w2241: invariant xabs <= 871.24
		when xabs = 871.24 sync F goto w2242;
	loc w2242: invariant xabs <= 871.36
		when xabs = 871.36 sync B goto w2243;
	loc w2243: invariant xabs <= 871.56
		when xabs = 871.56 sync C goto w2244;
	loc w2244: invariant xabs <= 871.72
		when xabs = 871.72 sync B goto w2245;
	loc w2245: invariant xabs <= 872.04
		when xabs = 872.04 sync C goto w2246;
	loc w2246: invariant xabs <= 872.52
		when xabs = 872.52 sync B goto w2247;
	loc w2247: invariant xabs <= 872.6
		when xabs = 872.6 sync A goto w2248;
	loc w2248: invariant xabs <= 872.68
		when xabs = 872.68 sync F goto w2249;
	loc w2249: invariant xabs <= 872.72
		when xabs = 872.72 sync E goto w2250;
	loc w2250: invariant xabs <= 873
		when xabs = 873 sync B goto w2251;
	loc w2251: invariant xabs <= 873.08
		when xabs = 873.08 sync A goto w2252;
	loc w2252: invariant xabs <= 873.2
		when xabs = 873.2 sync F goto w2253;
	loc w2253: invariant xabs <= 873.24
		when xabs = 873.24 sync E goto w2254;
	loc w2254: invariant xabs <= 873.48
		when xabs = 873.48 sync B goto w2255;
	loc w2255: invariant xabs <= 873.56
		when xabs = 873.56 sync A goto w2256;
	loc w2256: invariant xabs <= 873.68
		when xabs = 873.68 sync F goto w2257;
	loc w2257: invariant xabs <= 873.72
		when xabs = 873.72 sync E goto w2258;
	loc w2258: invariant xabs <= 874
		when xabs = 874 sync B goto w2259;
	loc w2259: invariant xabs <= 874.04
		when xabs = 874.04 sync A goto w2260;
	loc w2260: invariant xabs <= 874.16
		when xabs = 874.16 sync F goto w2261;
	loc w2261: invariant xabs <= 874.2
		when xabs = 874.2 sync E goto w2262;
	loc w2262: invariant xabs <= 874.52
		when xabs = 874.52 sync B goto w2263;
	loc w2263: invariant xabs <= 874.56
		when xabs = 874.56 sync A goto w2264;
	loc w2264: invariant xabs <= 874.6
		when xabs = 874.6 sync F goto w2265;
	loc w2265: invariant xabs <= 874.68
		when xabs = 874.68 sync E goto w2266;
	loc w2266: invariant xabs <= 875
		when xabs = 875 sync B goto w2267;
	loc w2267: invariant xabs <= 875.16
		when xabs = 875.16 sync A goto w2268;
	loc w2268: invariant xabs <= 875.48
		when xabs = 875.48 sync B goto w2269;
	loc w2269: invariant xabs <= 875.56
		when xabs = 875.56 sync A goto w2270;
	loc w2270: invariant xabs <= 875.6
		when xabs = 875.6 sync F goto w2271;
	loc w2271: invariant xabs <= 875.64
		when xabs = 875.64 sync E goto w2272;
	loc w2272: invariant xabs <= 875.96
		when xabs = 875.96 sync B goto w2273;
	loc w2273: invariant xabs <= 876
		when xabs = 876 sync A goto w2274;
	loc w2274: invariant xabs <= 876.12
		when xabs = 876.12 sync F goto w2275;
	loc w2275: invariant xabs <= 876.16
		when xabs = 876.16 sync E goto w2276;
	loc w2276: invariant xabs <= 876.44
		when xabs = 876.44 sync B goto w2277;
	loc w2277: invariant xabs <= 876.48
		when xabs = 876.48 sync A goto w2278;
	loc w2278: invariant xabs <= 876.6
		when xabs = 876.6 sync F goto w2279;
	loc w2279: invariant xabs <= 876.64
		when xabs = 876.64 sync E goto w2280;
	loc w2280: invariant xabs <= 876.92
		when xabs = 876.92 sync B goto w2281;
	loc w2281: invariant xabs <= 877
		when xabs = 877 sync A goto w2282;
	loc w2282: invariant xabs <= 877.08
		when xabs = 877.08 sync F goto w2283;
	loc w2283: invariant xabs <= 877.12
		when xabs = 877.12 sync E goto w2284;
	loc w2284: invariant xabs <= 877.44
		when xabs = 877.44 sync B goto w2285;
	loc w2285: invariant xabs <= 877.48
		when xabs = 877.48 sync A goto w2286;
	loc w2286: invariant xabs <= 877.56
		when xabs = 877.56 sync F goto w2287;
	loc w2287: invariant xabs <= 877.6
		when xabs = 877.6 sync E goto w2288;
	loc w2288: invariant xabs <= 877.96
		when xabs = 877.96 sync B goto w2289;
	loc w2289: invariant xabs <= 878.08
		when xabs = 878.08 sync A goto w2290;
	loc w2290: invariant xabs <= 878.28
		when xabs = 878.28 sync B goto w2291;
	loc w2291: invariant xabs <= 883
		when xabs = 883 sync A goto w2292;
	loc w2292: invariant xabs <= 883.32
		when xabs = 883.32 sync B goto w2293;
	loc w2293: invariant xabs <= 883.48
		when xabs = 883.48 sync A goto w2294;
	loc w2294: invariant xabs <= 883.8
		when xabs = 883.8 sync B goto w2295;
	loc w2295: invariant xabs <= 883.96
		when xabs = 883.96 sync A goto w2296;
	loc w2296: invariant xabs <= 884.32
		when xabs = 884.32 sync B goto w2297;
	loc w2297: invariant xabs <= 884.44
		when xabs = 884.44 sync A goto w2298;
	loc w2298: invariant xabs <= 884.8
		when xabs = 884.8 sync B goto w2299;
	loc w2299: invariant xabs <= 884.96
		when xabs = 884.96 sync A goto w2300;
	loc w2300: invariant xabs <= 885.28
		when xabs = 885.28 sync B goto w2301;
	loc w2301: invariant xabs <= 886
		when xabs = 886 sync A goto w2302;
	loc w2302: invariant xabs <= 886.24
		when xabs = 886.24 sync B goto w2303;
	loc w2303: invariant xabs <= 886.44
		when xabs = 886.44 sync A goto w2304;
	loc w2304: invariant xabs <= 886.76
		when xabs = 886.76 sync B goto w2305;
	loc w2305: invariant xabs <= 886.92
		when xabs = 886.92 sync A goto w2306;
	loc w2306: invariant xabs <= 887.24
		when xabs = 887.24 sync B goto w2307;
	loc w2307: invariant xabs <= 887.4
		when xabs = 887.4 sync A goto w2308;
	loc w2308: invariant xabs <= 887.76
		when xabs = 887.76 sync B goto w2309;
	loc w2309: invariant xabs <= 887.88
		when xabs = 887.88 sync A goto w2310;
	loc w2310: invariant xabs <= 888.24
		when xabs = 888.24 sync B goto w2311;
	loc w2311: invariant xabs <= 888.4
		when xabs = 888.4 sync A goto w2312;
	loc w2312: invariant xabs <= 888.72
		when xabs = 888.72 sync B goto w2313;
	loc w2313: invariant xabs <= 888.88
		when xabs = 888.88 sync A goto w2314;
	loc w2314: invariant xabs <= 889.2
		when xabs = 889.2 sync B goto w2315;
	loc w2315: invariant xabs <= 889.36
		when xabs = 889.36 sync A goto w2316;
	loc w2316: invariant xabs <= 889.68
		when xabs = 889.68 sync B goto w2317;
	loc w2317: invariant xabs <= 889.84
		when xabs = 889.84 sync A goto w2318;
	loc w2318: invariant xabs <= 890.2
		when xabs = 890.2 sync B goto w2319;
	loc w2319: invariant xabs <= 890.32
		when xabs = 890.32 sync A goto w2320;
	loc w2320: invariant xabs <= 891.16
		when xabs = 891.16 sync B goto w2321;
	loc w2321: invariant xabs <= 891.32
		when xabs = 891.32 sync A goto w2322;
	loc w2322: invariant xabs <= 891.64
		when xabs = 891.64 sync B goto w2323;
	loc w2323: invariant xabs <= 892.36
		when xabs = 892.36 sync A goto w2324;
	loc w2324: invariant xabs <= 892.6
		when xabs = 892.6 sync B goto w2325;
	loc w2325: invariant xabs <= 895.72
		when xabs = 895.72 sync A goto w2326;
	loc w2326: invariant xabs <= 896.04
		when xabs = 896.04 sync B goto w2327;
	loc w2327: invariant xabs <= 896.2
		when xabs = 896.2 sync A goto w2328;
	loc w2328: invariant xabs <= 896.56
		when xabs = 896.56 sync B goto w2329;
	loc w2329: invariant xabs <= 896.68
		when xabs = 896.68 sync A goto w2330;
	loc w2330: invariant xabs <= 897.04
		when xabs = 897.04 sync B goto w2331;
	loc w2331: invariant xabs <= 921.2
		when xabs = 921.2 sync A goto w2332;
	loc w2332: invariant xabs <= 921.48
		when xabs = 921.48 sync B goto w2333;
	loc w2333: invariant xabs <= 921.68
		when xabs = 921.68 sync A goto w2334;
	loc w2334: invariant xabs <= 922
		when xabs = 922 sync B goto w2335;
	loc w2335: invariant xabs <= 922.16
		when xabs = 922.16 sync A goto w2336;
	loc w2336: invariant xabs <= 922.48
		when xabs = 922.48 sync B goto w2337;
	loc w2337: invariant xabs <= 922.68
		when xabs = 922.68 sync A goto w2338;
	loc w2338: invariant xabs <= 922.96
		when xabs = 922.96 sync B goto w2339;
	loc w2339: invariant xabs <= 923.2
		when xabs = 923.2 sync A goto w2340;
	loc w2340: invariant xabs <= 923.44
		when xabs = 923.44 sync B goto w2341;
	loc w2341: invariant xabs <= 923.56
		when xabs = 923.56 sync A goto w2342;
	loc w2342: invariant xabs <= 923.6
		when xabs = 923.6 sync F goto w2343;
	loc w2343: invariant xabs <= 923.68
		when xabs = 923.68 sync E goto w2344;
	loc w2344: invariant xabs <= 923.92
		when xabs = 923.92 sync B goto w2345;
	loc w2345: invariant xabs <= 924.04
		when xabs = 924.04 sync A goto w2346;
	loc w2346: invariant xabs <= 924.08
		when xabs = 924.08 sync F goto w2347;
	loc w2347: invariant xabs <= 924.16
		when xabs = 924.16 sync E goto w2348;
	loc w2348: invariant xabs <= 924.4
		when xabs = 924.4 sync B goto w2349;
	loc w2349: invariant xabs <= 924.52
		when xabs = 924.52 sync A goto w2350;
	loc w2350: invariant xabs <= 924.56
		when xabs = 924.56 sync F goto w2351;
	loc w2351: invariant xabs <= 924.64
		when xabs = 924.64 sync E goto w2352;
	loc w2352: invariant xabs <= 924.92
		when xabs = 924.92 sync B goto w2353;
	loc w2353: invariant xabs <= 925.12
		when xabs = 925.12 sync A goto w2354;
	loc w2354: invariant xabs <= 925.4
		when xabs = 925.4 sync B goto w2355;
	loc w2355: invariant xabs <= 925.6
		when xabs = 925.6 sync A goto w2356;
	loc w2356: invariant xabs <= 925.88
		when xabs = 925.88 sync B goto w2357;
	loc w2357: invariant xabs <= 925.96
		when xabs = 925.96 sync A goto w2358;
	loc w2358: invariant xabs <= 926.04
		when xabs = 926.04 sync F goto w2359;
	loc w2359: invariant xabs <= 926.12
		when xabs = 926.12 sync E goto w2360;
	loc w2360: invariant xabs <= 926.36
		when xabs = 926.36 sync B goto w2361;
	loc w2361: invariant xabs <= 926.44
		when xabs = 926.44 sync A goto w2362;
	loc w2362: invariant xabs <= 926.56
		when xabs = 926.56 sync F goto w2363;
	loc w2363: invariant xabs <= 926.6
		when xabs = 926.6 sync E goto w2364;
	loc w2364: invariant xabs <= 926.84
		when xabs = 926.84 sync B goto w2365;
	loc w2365: invariant xabs <= 926.92
		when xabs = 926.92 sync A goto w2366;
	loc w2366: invariant xabs <= 927.08
		when xabs = 927.08 sync F goto w2367;
	loc w2367: invariant xabs <= 927.12
		when xabs = 927.12 sync E goto w2368;
	loc w2368: invariant xabs <= 927.36
		when xabs = 927.36 sync B goto w2369;
	loc w2369: invariant xabs <= 927.4
		when xabs = 927.4 sync A goto w2370;
	loc w2370: invariant xabs <= 927.56
		when xabs = 927.56 sync F goto w2371;
	loc w2371: invariant xabs <= 927.6
		when xabs = 927.6 sync E goto w2372;
	loc w2372: invariant xabs <= 927.72
		when xabs = 927.72 sync B goto w2373;
	loc w2373: invariant xabs <= 927.84
		when xabs = 927.84 sync C goto w2374;
	loc w2374: invariant xabs <= 927.92
		when xabs = 927.92 sync B goto w2375;
	loc w2375: invariant xabs <= 928
		when xabs = 928 sync F goto w2376;
	loc w2376: invariant xabs <= 928.08
		when xabs = 928.08 sync E goto w2377;
	loc w2377: invariant xabs <= 928.32
		when xabs = 928.32 sync C goto w2378;
	loc w2378: invariant xabs <= 928.4
		when xabs = 928.4 sync B goto w2379;
	loc w2379: invariant xabs <= 928.48
		when xabs = 928.48 sync F goto w2380;
	loc w2380: invariant xabs <= 928.56
		when xabs = 928.56 sync E goto w2381;
	loc w2381: invariant xabs <= 928.84
		when xabs = 928.84 sync C goto w2382;
	loc w2382: invariant xabs <= 928.92
		when xabs = 928.92 sync B goto w2383;
	loc w2383: invariant xabs <= 929
		when xabs = 929 sync F goto w2384;
	loc w2384: invariant xabs <= 929.04
		when xabs = 929.04 sync E goto w2385;
	loc w2385: invariant xabs <= 929.32
		when xabs = 929.32 sync C goto w2386;
	loc w2386: invariant xabs <= 929.4
		when xabs = 929.4 sync B goto w2387;
	loc w2387: invariant xabs <= 929.52
		when xabs = 929.52 sync F goto w2388;
	loc w2388: invariant xabs <= 929.56
		when xabs = 929.56 sync E goto w2389;
	loc w2389: invariant xabs <= 929.76
		when xabs = 929.76 sync C goto w2390;
	loc w2390: invariant xabs <= 929.84
		when xabs = 929.84 sync B goto w2391;
	loc w2391: invariant xabs <= 930
		when xabs = 930 sync F goto w2392;
	loc w2392: invariant xabs <= 930.04
		when xabs = 930.04 sync E goto w2393;
	loc w2393: invariant xabs <= 930.28
		when xabs = 930.28 sync C goto w2394;
	loc w2394: invariant xabs <= 930.36
		when xabs = 930.36 sync B goto w2395;
	loc w2395: invariant xabs <= 930.48
		when xabs = 930.48 sync F goto w2396;
	loc w2396: invariant xabs <= 930.52
		when xabs = 930.52 sync E goto w2397;
	loc w2397: invariant xabs <= 930.76
		when xabs = 930.76 sync C goto w2398;
	loc w2398: invariant xabs <= 930.84
		when xabs = 930.84 sync B goto w2399;
	loc w2399: invariant xabs <= 930.96
		when xabs = 930.96 sync F goto w2400;
	loc w2400: invariant xabs <= 931
		when xabs = 931 sync E goto w2401;
	loc w2401: invariant xabs <= 931.28
		when xabs = 931.28 sync C goto w2402;
	loc w2402: invariant xabs <= 931.36
		when xabs = 931.36 sync B goto w2403;
	loc w2403: invariant xabs <= 931.44
		when xabs = 931.44 sync F goto w2404;
	loc w2404: invariant xabs <= 931.52
		when xabs = 931.52 sync E goto w2405;
	loc w2405: invariant xabs <= 931.76
		when xabs = 931.76 sync C goto w2406;
	loc w2406: invariant xabs <= 931.8
		when xabs = 931.8 sync B goto w2407;
	loc w2407: invariant xabs <= 931.96
		when xabs = 931.96 sync F goto w2408;
	loc w2408: invariant xabs <= 932
		when xabs = 932 sync E goto w2409;
	loc w2409: invariant xabs <= 932.24
		when xabs = 932.24 sync C goto w2410;
	loc w2410: invariant xabs <= 932.32
		when xabs = 932.32 sync B goto w2411;
	loc w2411: invariant xabs <= 932.44
		when xabs = 932.44 sync F goto w2412;
	loc w2412: invariant xabs <= 932.52
		when xabs = 932.52 sync E goto w2413;
	loc w2413: invariant xabs <= 932.72
		when xabs = 932.72 sync C goto w2414;
	loc w2414: invariant xabs <= 932.76
		when xabs = 932.76 sync B goto w2415;
	loc w2415: invariant xabs <= 932.96
		when xabs = 932.96 sync F goto w2416;
	loc w2416: invariant xabs <= 933
		when xabs = 933 sync E goto w2417;
	loc w2417: invariant xabs <= 933.2
		when xabs = 933.2 sync C goto w2418;
	loc w2418: invariant xabs <= 933.24
		when xabs = 933.24 sync B goto w2419;
	loc w2419: invariant xabs <= 933.44
		when xabs = 933.44 sync F goto w2420;
	loc w2420: invariant xabs <= 933.48
		when xabs = 933.48 sync E goto w2421;
	loc w2421: invariant xabs <= 933.68
		when xabs = 933.68 sync C goto w2422;
	loc w2422: invariant xabs <= 933.76
		when xabs = 933.76 sync B goto w2423;
	loc w2423: invariant xabs <= 933.92
		when xabs = 933.92 sync F goto w2424;
	loc w2424: invariant xabs <= 933.96
		when xabs = 933.96 sync E goto w2425;
	loc w2425: invariant xabs <= 934.2
		when xabs = 934.2 sync C goto w2426;
	loc w2426: invariant xabs <= 934.24
		when xabs = 934.24 sync B goto w2427;
	loc w2427: invariant xabs <= 934.4
		when xabs = 934.4 sync F goto w2428;
	loc w2428: invariant xabs <= 934.44
		when xabs = 934.44 sync E goto w2429;
	loc w2429: invariant xabs <= 934.68
		when xabs = 934.68 sync C goto w2430;
	loc w2430: invariant xabs <= 934.76
		when xabs = 934.76 sync B goto w2431;
	loc w2431: invariant xabs <= 934.88
		when xabs = 934.88 sync F goto w2432;
	loc w2432: invariant xabs <= 934.92
		when xabs = 934.92 sync E goto w2433;
	loc w2433: invariant xabs <= 935.2
		when xabs = 935.2 sync C goto w2434;
	loc w2434: invariant xabs <= 935.24
		when xabs = 935.24 sync B goto w2435;
	loc w2435: invariant xabs <= 935.4
		when xabs = 935.4 sync F goto w2436;
	loc w2436: invariant xabs <= 935.44
		when xabs = 935.44 sync E goto w2437;
	loc w2437: invariant xabs <= 935.64
		when xabs = 935.64 sync C goto w2438;
	loc w2438: invariant xabs <= 935.72
		when xabs = 935.72 sync B goto w2439;
	loc w2439: invariant xabs <= 935.92
		when xabs = 935.92 sync F goto w2440;
	loc w2440: invariant xabs <= 935.96
		when xabs = 935.96 sync E goto w2441;
	loc w2441: invariant xabs <= 936.12
		when xabs = 936.12 sync C goto w2442;
	loc w2442: invariant xabs <= 936.16
		when xabs = 936.16 sync B goto w2443;
	loc w2443: invariant xabs <= 936.4
		when xabs = 936.4 sync F goto w2444;
	loc w2444: invariant xabs <= 936.44
		when xabs = 936.44 sync E goto w2445;
	loc w2445: invariant xabs <= 936.6
		when xabs = 936.6 sync C goto w2446;
	loc w2446: invariant xabs <= 936.68
		when xabs = 936.68 sync B goto w2447;
	loc w2447: invariant xabs <= 936.88
		when xabs = 936.88 sync F goto w2448;
	loc w2448: invariant xabs <= 936.92
		when xabs = 936.92 sync E goto w2449;
	loc w2449: invariant xabs <= 937.12
		when xabs = 937.12 sync C goto w2450;
	loc w2450: invariant xabs <= 937.16
		when xabs = 937.16 sync B goto w2451;
	loc w2451: invariant xabs <= 937.36
		when xabs = 937.36 sync F goto w2452;
	loc w2452: invariant xabs <= 937.4
		when xabs = 937.4 sync E goto w2453;
	loc w2453: invariant xabs <= 937.64
		when xabs = 937.64 sync C goto w2454;
	loc w2454: invariant xabs <= 937.68
		when xabs = 937.68 sync B goto w2455;
	loc w2455: invariant xabs <= 937.84
		when xabs = 937.84 sync F goto w2456;
	loc w2456: invariant xabs <= 937.88
		when xabs = 937.88 sync E goto w2457;
	loc w2457: invariant xabs <= 938.16
		when xabs = 938.16 sync C goto w2458;
	loc w2458: invariant xabs <= 938.28
		when xabs = 938.28 sync B goto w2459;
	loc w2459: invariant xabs <= 940.88
		when xabs = 940.88 sync A goto w2460;
	loc w2460: invariant xabs <= 941.04
		when xabs = 941.04 sync B goto w2461;
	loc w2461: invariant xabs <= 941.32
		when xabs = 941.32 sync A goto w2462;
	loc w2462: invariant xabs <= 941.52
		when xabs = 941.52 sync B goto w2463;
	loc w2463: invariant xabs <= 941.64
		when xabs = 941.64 sync A goto w2464;
	loc w2464: invariant xabs <= 941.76
		when xabs = 941.76 sync F goto w2465;
	loc w2465: invariant xabs <= 941.84
		when xabs = 941.84 sync E goto w2466;
	loc w2466: invariant xabs <= 942
		when xabs = 942 sync B goto w2467;
	loc w2467: invariant xabs <= 942.08
		when xabs = 942.08 sync A goto w2468;
	loc w2468: invariant xabs <= 942.28
		when xabs = 942.28 sync F goto w2469;
	loc w2469: invariant xabs <= 942.32
		when xabs = 942.32 sync E goto w2470;
	loc w2470: invariant xabs <= 942.48
		when xabs = 942.48 sync B goto w2471;
	loc w2471: invariant xabs <= 942.56
		when xabs = 942.56 sync A goto w2472;
	loc w2472: invariant xabs <= 942.8
		when xabs = 942.8 sync F goto w2473;
	loc w2473: invariant xabs <= 942.84
		when xabs = 942.84 sync E goto w2474;
	loc w2474: invariant xabs <= 942.96
		when xabs = 942.96 sync B goto w2475;
	loc w2475: invariant xabs <= 943
		when xabs = 943 sync A goto w2476;
	loc w2476: invariant xabs <= 943.28
		when xabs = 943.28 sync F goto w2477;
	loc w2477: invariant xabs <= 943.32
		when xabs = 943.32 sync E goto w2478;
	loc w2478: invariant xabs <= 943.48
		when xabs = 943.48 sync B goto w2479;
	loc w2479: invariant xabs <= 943.52
		when xabs = 943.52 sync A goto w2480;
	loc w2480: invariant xabs <= 943.76
		when xabs = 943.76 sync F goto w2481;
	loc w2481: invariant xabs <= 943.96
		when xabs = 943.96 sync B goto w2482;
	loc w2482: invariant xabs <= 944.04
		when xabs = 944.04 sync A goto w2483;
	loc w2483: invariant xabs <= 944.24
		when xabs = 944.24 sync F goto w2484;
	loc w2484: invariant xabs <= 944.52
		when xabs = 944.52 sync B goto w2485;
	loc w2485: invariant xabs <= 944.72
		when xabs = 944.72 sync F goto w2486;
	loc w2486: invariant xabs <= 944.76
		when xabs = 944.76 sync E goto w2487;
	loc w2487: invariant xabs <= 944.92
		when xabs = 944.92 sync C goto w2488;
	loc w2488: invariant xabs <= 945
		when xabs = 945 sync B goto w2489;
	loc w2489: invariant xabs <= 945.24
		when xabs = 945.24 sync F goto w2490;
	loc w2490: invariant xabs <= 945.28
		when xabs = 945.28 sync E goto w2491;
	loc w2491: invariant xabs <= 945.4
		when xabs = 945.4 sync C goto w2492;
	loc w2492: invariant xabs <= 945.44
		when xabs = 945.44 sync B goto w2493;
	loc w2493: invariant xabs <= 945.76
		when xabs = 945.76 sync F goto w2494;
	loc w2494: invariant xabs <= 945.84
		when xabs = 945.84 sync C goto w2495;
	loc w2495: invariant xabs <= 945.88
		when xabs = 945.88 sync F goto w2496;
	loc w2496: invariant xabs <= 946.24
		when xabs = 946.24 sync B goto w2497;
	loc w2497: invariant xabs <= 946.4
		when xabs = 946.4 sync C goto w2498;
	loc w2498: invariant xabs <= 946.68
		when xabs = 946.68 sync F goto w2499;
	loc w2499: invariant xabs <= 946.72
		when xabs = 946.72 sync E goto w2500;
	loc w2500: invariant xabs <= 946.88
		when xabs = 946.88 sync D goto w2501;
	loc w2501: invariant xabs <= 946.96
		when xabs = 946.96 sync C goto w2502;
	loc w2502: invariant xabs <= 947.16
		when xabs = 947.16 sync F goto w2503;
	loc w2503: invariant xabs <= 947.2
		when xabs = 947.2 sync E goto w2504;
	loc w2504: invariant xabs <= 947.4
		when xabs = 947.4 sync D goto w2505;
	loc w2505: invariant xabs <= 947.44
		when xabs = 947.44 sync C goto w2506;
	loc w2506: invariant xabs <= 947.68
		when xabs = 947.68 sync F goto w2507;
	loc w2507: invariant xabs <= 947.72
		when xabs = 947.72 sync E goto w2508;
	loc w2508: invariant xabs <= 947.88
		when xabs = 947.88 sync D goto w2509;
	loc w2509: invariant xabs <= 947.92
		when xabs = 947.92 sync C goto w2510;
	loc w2510: invariant xabs <= 948.2
		when xabs = 948.2 sync F goto w2511;
	loc w2511: invariant xabs <= 948.28
		when xabs = 948.28 sync E goto w2512;
	loc w2512: invariant xabs <= 949.2
		when xabs = 949.2 sync F goto w2513;
	loc w2513: invariant xabs <= 949.24
		when xabs = 949.24 sync E goto w2514;
	loc w2514: invariant xabs <= 949.68
		when xabs = 949.68 sync F goto w2515;
	loc w2515: invariant xabs <= 949.8
		when xabs = 949.8 sync D goto w2516;
	loc w2516: invariant xabs <= 949.84
		when xabs = 949.84 sync C goto w2517;
	loc w2517: invariant xabs <= 950.12
		when xabs = 950.12 sync F goto w2518;
	loc w2518: invariant xabs <= 950.16
		when xabs = 950.16 sync E goto w2519;
	loc w2519: invariant xabs <= 950.32
		when xabs = 950.32 sync D goto w2520;
	loc w2520: invariant xabs <= 950.36
		when xabs = 950.36 sync C goto w2521;
	loc w2521: invariant xabs <= 950.64
		when xabs = 950.64 sync F goto w2522;
	loc w2522: invariant xabs <= 950.8
		when xabs = 950.8 sync D goto w2523;
	loc w2523: invariant xabs <= 950.84
		when xabs = 950.84 sync C goto w2524;
	loc w2524: invariant xabs <= 951.16
		when xabs = 951.16 sync F goto w2525;
	loc w2525: invariant xabs <= 951.28
		when xabs = 951.28 sync D goto w2526;
	loc w2526: invariant xabs <= 953.12
		when xabs = 953.12 sync C goto w2527;
	loc w2527: invariant xabs <= 953.56
		when xabs = 953.56 sync D goto w2528;
	loc w2528: invariant xabs <= 953.76
		when xabs = 953.76 sync E goto w2529;
	loc w2529: invariant xabs <= 954.08
		when xabs = 954.08 sync F goto w2530;
	loc w2530: invariant xabs <= 954.16
		when xabs = 954.16 sync E goto w2531;
	loc w2531: invariant xabs <= 956.52
		when xabs = 956.52 sync F goto w2532;
	loc w2532: invariant xabs <= 956.6
		when xabs = 956.6 sync E goto w2533;
	loc w2533: invariant xabs <= 957.36
		when xabs = 957.36 sync F goto w2534;
	loc w2534: invariant xabs <= 958
		when xabs = 958 sync H goto w2535;
	loc w2535: invariant xabs <= 958.04
		when xabs = 958.04 sync E goto w2536;
	loc w2536: invariant xabs <= 958.24
		when xabs = 958.24 sync G goto w2537;
	loc w2537: invariant xabs <= 958.36
		when xabs = 958.36 sync C goto w2538;
	loc w2538: invariant xabs <= 958.52
		when xabs = 958.52 sync B goto w2539;
	loc w2539: invariant xabs <= 960.52
		when xabs = 960.52 sync A goto w2540;
	loc w2540: invariant xabs <= 961.56
		when xabs = 961.56 sync F goto w2541;
	loc w2541: invariant xabs <= 963.72
		when xabs = 963.72 sync B goto w2542;
	loc w2542: invariant xabs <= 966.68
		when xabs = 966.68 sync C goto w2543;
	loc w2543: invariant xabs <= 966.76
		when xabs = 966.76 sync H goto w2544;
	loc w2544: invariant xabs <= 978
		when xabs = 978 sync D goto w2545;
	loc w2545: invariant xabs <= 978.12
		when xabs = 978.12 sync E goto w2546;
	loc w2546: invariant xabs <= 978.32
		when xabs = 978.32 sync G goto w2547;
	loc w2547: invariant xabs <= 978.44
		when xabs = 978.44 sync C goto w2548;
	loc w2548: invariant xabs <= 978.56
		when xabs = 978.56 sync B goto w2549;
	loc w2549: invariant xabs <= 980.36
		when xabs = 980.36 sync A goto w2550;
	loc w2550: invariant xabs <= 981.32
		when xabs = 981.32 sync F goto w2551;
	loc w2551: invariant xabs <= 982.8
		when xabs = 982.8 sync B goto w2552;
	loc w2552: invariant xabs <= 984.8
		when xabs = 984.8 sync C goto w2553;
	loc w2553: invariant xabs <= 984.88
		when xabs = 984.88 sync H goto w2554;
	loc w2554: invariant xabs <= 998
		when xabs = 998 sync D goto w2555;
	loc w2555: invariant xabs <= 998.12
		when xabs = 998.12 sync E goto w2556;
	loc w2556: invariant xabs <= 998.32
		when xabs = 998.32 sync G goto w2557;
	loc w2557: invariant xabs <= 998.44
		when xabs = 998.44 sync C goto w2558;
	loc w2558: invariant xabs <= 998.56
		when xabs = 998.56 sync B goto w2559;
	loc w2559: invariant xabs <= 1000
		when xabs = 1000 sync A goto w2560;

	loc w2560: invariant True
end (* word *)

(************************************************************)
(* Initial state *)
(************************************************************)

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	& loc[pta] = pre_s0
	& loc[word] = w1

	(*------------------------------------------------------------*)
	(* Initial clock constraints *)
	(*------------------------------------------------------------*)
	& x = 0
	& xabs = 0

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
	& p10 >= 0
	& t >= 0
	& tprime >= 0
;

(************************************************************)
(* The end *)
(************************************************************)
end