// This file is part of the SV-Benchmarks collection of verification tasks: // https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks // // SPDX-FileCopyrightText: 2019 Makai Mann // SPDX-FileCopyrightText: 2022 The SV-Benchmarks Community // // SPDX-License-Identifier: BSD-3-Clause // This C program is converted from Btor2 by Btor2C version sha1:a0fa249 // with arguments: { architecture=64, lazy_modulo=true, use_memmove=false, unroll_inner_loops=false, shortest_type=true, diff_type=true, decimal_constant=true, zero_init=false, sra_extend_sign=true } // Comments from the original Btor2 file: // ; source: https://github.com/makaimann/btor-benchmarks/tree/d9a2792dcee39f17607c889500ac76ad3df35a50 // ; BTOR description generated by Yosys 0.8+612 (git sha1 d6a289d3, g++ 9.1.1 -Os) for module circular_pointer_top. extern unsigned char __VERIFIER_nondet_uchar(); extern unsigned short __VERIFIER_nondet_ushort(); extern unsigned int __VERIFIER_nondet_uint(); extern unsigned long __VERIFIER_nondet_ulong(); extern void abort(void); extern void __assert_fail(const char *, const char *, unsigned int, const char *); void reach_error() { __assert_fail("0", "circular_pointer_top_w16_d16_e0.c", 0, "reach_error"); } void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: { reach_error(); abort(); } } } void assume_abort_if_not(int cond) { if (!cond) { abort(); } } int main() { // Defining sorts ... typedef unsigned char SORT_1; // BV with 1 bits const SORT_1 mask_SORT_1 = (SORT_1)-1 >> (sizeof(SORT_1) * 8 - 1); const SORT_1 msb_SORT_1 = (SORT_1)1 << (1 - 1); typedef unsigned short SORT_3; // BV with 16 bits const SORT_3 mask_SORT_3 = (SORT_3)-1 >> (sizeof(SORT_3) * 8 - 16); const SORT_3 msb_SORT_3 = (SORT_3)1 << (16 - 1); typedef unsigned char SORT_11; // BV with 6 bits const SORT_11 mask_SORT_11 = (SORT_11)-1 >> (sizeof(SORT_11) * 8 - 6); const SORT_11 msb_SORT_11 = (SORT_11)1 << (6 - 1); typedef unsigned char SORT_13; // BV with 5 bits const SORT_13 mask_SORT_13 = (SORT_13)-1 >> (sizeof(SORT_13) * 8 - 5); const SORT_13 msb_SORT_13 = (SORT_13)1 << (5 - 1); typedef unsigned char SORT_19; // BV with 4 bits const SORT_19 mask_SORT_19 = (SORT_19)-1 >> (sizeof(SORT_19) * 8 - 4); const SORT_19 msb_SORT_19 = (SORT_19)1 << (4 - 1); typedef unsigned char SORT_60; // BV with 3 bits const SORT_60 mask_SORT_60 = (SORT_60)-1 >> (sizeof(SORT_60) * 8 - 3); const SORT_60 msb_SORT_60 = (SORT_60)1 << (3 - 1); typedef unsigned char SORT_81; // BV with 2 bits const SORT_81 mask_SORT_81 = (SORT_81)-1 >> (sizeof(SORT_81) * 8 - 2); const SORT_81 msb_SORT_81 = (SORT_81)1 << (2 - 1); // Initializing constants ... const SORT_13 var_15 = 16; const SORT_19 var_20 = 15; const SORT_19 var_25 = 14; const SORT_19 var_30 = 13; const SORT_19 var_35 = 12; const SORT_19 var_40 = 11; const SORT_19 var_45 = 10; const SORT_19 var_50 = 9; const SORT_19 var_55 = 8; const SORT_60 var_61 = 7; const SORT_60 var_66 = 6; const SORT_60 var_71 = 5; const SORT_60 var_76 = 4; const SORT_81 var_82 = 3; const SORT_81 var_87 = 2; const SORT_1 var_92 = 1; const SORT_13 var_105 = 17; const SORT_11 var_122 = 0; const SORT_1 var_152 = 0; const SORT_3 var_373 = 0; // Collecting input declarations ... SORT_1 input_2; SORT_3 input_4; SORT_1 input_5; SORT_1 input_6; SORT_1 input_7; SORT_1 input_8; SORT_3 input_9; SORT_1 input_150; // Collecting state declarations ... SORT_3 state_10 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_11 state_12 = __VERIFIER_nondet_uchar() & mask_SORT_11; SORT_3 state_18 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_24 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_29 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_34 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_39 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_44 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_49 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_54 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_59 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_65 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_70 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_75 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_80 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_86 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_91 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_3 state_96 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_11 state_101 = __VERIFIER_nondet_uchar() & mask_SORT_11; SORT_1 state_109 = __VERIFIER_nondet_uchar() & mask_SORT_1; SORT_1 state_110 = __VERIFIER_nondet_uchar() & mask_SORT_1; SORT_11 state_113 = __VERIFIER_nondet_uchar() & mask_SORT_11; SORT_3 state_128 = __VERIFIER_nondet_ushort() & mask_SORT_3; SORT_1 state_132 = __VERIFIER_nondet_uchar() & mask_SORT_1; SORT_11 state_185 = __VERIFIER_nondet_uchar() & mask_SORT_11; // Initializing states ... SORT_1 init_133_arg_1 = var_92; state_132 = init_133_arg_1; for (;;) { // Getting external input values ... input_2 = __VERIFIER_nondet_uchar(); input_4 = __VERIFIER_nondet_ushort(); input_5 = __VERIFIER_nondet_uchar(); input_6 = __VERIFIER_nondet_uchar(); input_7 = __VERIFIER_nondet_uchar(); input_7 = input_7 & mask_SORT_1; input_8 = __VERIFIER_nondet_uchar(); input_9 = __VERIFIER_nondet_ushort(); input_150 = __VERIFIER_nondet_uchar(); // Assuming invariants ... SORT_1 var_134_arg_0 = input_7; SORT_1 var_134_arg_1 = state_132; SORT_1 var_134 = var_134_arg_0 == var_134_arg_1; SORT_1 var_135_arg_0 = var_92; SORT_1 var_135 = ~var_135_arg_0; SORT_1 var_136_arg_0 = var_134; SORT_1 var_136_arg_1 = var_135; SORT_1 var_136 = var_136_arg_0 | var_136_arg_1; var_136 = var_136 & mask_SORT_1; SORT_1 constr_137_arg_0 = var_136; assume_abort_if_not(constr_137_arg_0); SORT_13 var_106_arg_0 = var_105; var_106_arg_0 = var_106_arg_0 & mask_SORT_13; SORT_11 var_106 = var_106_arg_0; SORT_11 var_107_arg_0 = state_101; SORT_11 var_107_arg_1 = var_106; SORT_1 var_107 = var_107_arg_0 == var_107_arg_1; SORT_1 var_138_arg_0 = var_107; SORT_1 var_138 = ~var_138_arg_0; SORT_1 var_139_arg_0 = input_6; SORT_1 var_139 = ~var_139_arg_0; SORT_1 var_140_arg_0 = var_138; SORT_1 var_140_arg_1 = var_139; SORT_1 var_140 = var_140_arg_0 | var_140_arg_1; SORT_1 var_141_arg_0 = var_92; SORT_1 var_141 = ~var_141_arg_0; SORT_1 var_142_arg_0 = var_140; SORT_1 var_142_arg_1 = var_141; SORT_1 var_142 = var_142_arg_0 | var_142_arg_1; var_142 = var_142 & mask_SORT_1; SORT_1 constr_143_arg_0 = var_142; assume_abort_if_not(constr_143_arg_0); SORT_11 var_102_arg_0 = state_101; SORT_1 var_102 = var_102_arg_0 != 0; SORT_1 var_103_arg_0 = var_102; SORT_1 var_103 = ~var_103_arg_0; SORT_1 var_144_arg_0 = var_103; SORT_1 var_144 = ~var_144_arg_0; SORT_1 var_145_arg_0 = input_5; SORT_1 var_145 = ~var_145_arg_0; SORT_1 var_146_arg_0 = var_144; SORT_1 var_146_arg_1 = var_145; SORT_1 var_146 = var_146_arg_0 | var_146_arg_1; SORT_1 var_147_arg_0 = var_92; SORT_1 var_147 = ~var_147_arg_0; SORT_1 var_148_arg_0 = var_146; SORT_1 var_148_arg_1 = var_147; SORT_1 var_148 = var_148_arg_0 | var_148_arg_1; var_148 = var_148 & mask_SORT_1; SORT_1 constr_149_arg_0 = var_148; assume_abort_if_not(constr_149_arg_0); // Asserting properties ... SORT_1 var_153_arg_0 = state_132; SORT_1 var_153_arg_1 = var_152; SORT_1 var_153_arg_2 = var_92; SORT_1 var_153 = var_153_arg_0 ? var_153_arg_1 : var_153_arg_2; SORT_1 var_111_arg_0 = state_110; SORT_1 var_111 = ~var_111_arg_0; SORT_1 var_112_arg_0 = state_109; SORT_1 var_112_arg_1 = var_111; SORT_1 var_112 = var_112_arg_0 & var_112_arg_1; SORT_11 var_114_arg_0 = state_113; SORT_1 var_114 = var_114_arg_0 != 0; SORT_1 var_115_arg_0 = var_112; SORT_1 var_115_arg_1 = var_114; SORT_1 var_115 = var_115_arg_0 & var_115_arg_1; SORT_1 var_116_arg_0 = state_109; SORT_1 var_116 = ~var_116_arg_0; SORT_1 var_117_arg_0 = input_6; SORT_1 var_117_arg_1 = var_116; SORT_1 var_117 = var_117_arg_0 & var_117_arg_1; SORT_1 var_118_arg_0 = var_117; var_118_arg_0 = var_118_arg_0 & mask_SORT_1; SORT_11 var_118 = var_118_arg_0; SORT_11 var_119_arg_0 = state_113; SORT_11 var_119_arg_1 = var_118; SORT_11 var_119 = var_119_arg_0 + var_119_arg_1; SORT_1 var_120_arg_0 = input_5; var_120_arg_0 = var_120_arg_0 & mask_SORT_1; SORT_11 var_120 = var_120_arg_0; SORT_11 var_121_arg_0 = var_119; SORT_11 var_121_arg_1 = var_120; SORT_11 var_121 = var_121_arg_0 - var_121_arg_1; SORT_1 var_123_arg_0 = input_7; SORT_11 var_123_arg_1 = var_122; SORT_11 var_123_arg_2 = var_121; SORT_11 var_123 = var_123_arg_0 ? var_123_arg_1 : var_123_arg_2; var_123 = var_123 & mask_SORT_11; SORT_11 var_124_arg_0 = var_123; SORT_1 var_124 = var_124_arg_0 != 0; SORT_1 var_125_arg_0 = var_124; SORT_1 var_125 = ~var_125_arg_0; SORT_1 var_126_arg_0 = var_115; SORT_1 var_126_arg_1 = var_125; SORT_1 var_126 = var_126_arg_0 & var_126_arg_1; SORT_1 var_127_arg_0 = var_126; SORT_1 var_127 = ~var_127_arg_0; SORT_11 var_14_arg_0 = state_12; SORT_13 var_14 = var_14_arg_0 >> 0; var_14 = var_14 & mask_SORT_13; SORT_13 var_97_arg_0 = var_14; SORT_1 var_97 = var_97_arg_0 != 0; SORT_1 var_98_arg_0 = var_97; SORT_1 var_98 = ~var_98_arg_0; var_98 = var_98 & mask_SORT_1; SORT_1 var_93_arg_0 = var_92; var_93_arg_0 = var_93_arg_0 & mask_SORT_1; SORT_13 var_93 = var_93_arg_0; SORT_13 var_94_arg_0 = var_14; SORT_13 var_94_arg_1 = var_93; SORT_1 var_94 = var_94_arg_0 == var_94_arg_1; SORT_81 var_88_arg_0 = var_87; var_88_arg_0 = var_88_arg_0 & mask_SORT_81; SORT_13 var_88 = var_88_arg_0; SORT_13 var_89_arg_0 = var_14; SORT_13 var_89_arg_1 = var_88; SORT_1 var_89 = var_89_arg_0 == var_89_arg_1; SORT_81 var_83_arg_0 = var_82; var_83_arg_0 = var_83_arg_0 & mask_SORT_81; SORT_13 var_83 = var_83_arg_0; SORT_13 var_84_arg_0 = var_14; SORT_13 var_84_arg_1 = var_83; SORT_1 var_84 = var_84_arg_0 == var_84_arg_1; SORT_60 var_77_arg_0 = var_76; var_77_arg_0 = var_77_arg_0 & mask_SORT_60; SORT_13 var_77 = var_77_arg_0; SORT_13 var_78_arg_0 = var_14; SORT_13 var_78_arg_1 = var_77; SORT_1 var_78 = var_78_arg_0 == var_78_arg_1; SORT_60 var_72_arg_0 = var_71; var_72_arg_0 = var_72_arg_0 & mask_SORT_60; SORT_13 var_72 = var_72_arg_0; SORT_13 var_73_arg_0 = var_14; SORT_13 var_73_arg_1 = var_72; SORT_1 var_73 = var_73_arg_0 == var_73_arg_1; SORT_60 var_67_arg_0 = var_66; var_67_arg_0 = var_67_arg_0 & mask_SORT_60; SORT_13 var_67 = var_67_arg_0; SORT_13 var_68_arg_0 = var_14; SORT_13 var_68_arg_1 = var_67; SORT_1 var_68 = var_68_arg_0 == var_68_arg_1; SORT_60 var_62_arg_0 = var_61; var_62_arg_0 = var_62_arg_0 & mask_SORT_60; SORT_13 var_62 = var_62_arg_0; SORT_13 var_63_arg_0 = var_14; SORT_13 var_63_arg_1 = var_62; SORT_1 var_63 = var_63_arg_0 == var_63_arg_1; SORT_19 var_56_arg_0 = var_55; var_56_arg_0 = var_56_arg_0 & mask_SORT_19; SORT_13 var_56 = var_56_arg_0; SORT_13 var_57_arg_0 = var_14; SORT_13 var_57_arg_1 = var_56; SORT_1 var_57 = var_57_arg_0 == var_57_arg_1; SORT_19 var_51_arg_0 = var_50; var_51_arg_0 = var_51_arg_0 & mask_SORT_19; SORT_13 var_51 = var_51_arg_0; SORT_13 var_52_arg_0 = var_14; SORT_13 var_52_arg_1 = var_51; SORT_1 var_52 = var_52_arg_0 == var_52_arg_1; SORT_19 var_46_arg_0 = var_45; var_46_arg_0 = var_46_arg_0 & mask_SORT_19; SORT_13 var_46 = var_46_arg_0; SORT_13 var_47_arg_0 = var_14; SORT_13 var_47_arg_1 = var_46; SORT_1 var_47 = var_47_arg_0 == var_47_arg_1; SORT_19 var_41_arg_0 = var_40; var_41_arg_0 = var_41_arg_0 & mask_SORT_19; SORT_13 var_41 = var_41_arg_0; SORT_13 var_42_arg_0 = var_14; SORT_13 var_42_arg_1 = var_41; SORT_1 var_42 = var_42_arg_0 == var_42_arg_1; SORT_19 var_36_arg_0 = var_35; var_36_arg_0 = var_36_arg_0 & mask_SORT_19; SORT_13 var_36 = var_36_arg_0; SORT_13 var_37_arg_0 = var_14; SORT_13 var_37_arg_1 = var_36; SORT_1 var_37 = var_37_arg_0 == var_37_arg_1; SORT_19 var_31_arg_0 = var_30; var_31_arg_0 = var_31_arg_0 & mask_SORT_19; SORT_13 var_31 = var_31_arg_0; SORT_13 var_32_arg_0 = var_14; SORT_13 var_32_arg_1 = var_31; SORT_1 var_32 = var_32_arg_0 == var_32_arg_1; SORT_19 var_26_arg_0 = var_25; var_26_arg_0 = var_26_arg_0 & mask_SORT_19; SORT_13 var_26 = var_26_arg_0; SORT_13 var_27_arg_0 = var_14; SORT_13 var_27_arg_1 = var_26; SORT_1 var_27 = var_27_arg_0 == var_27_arg_1; SORT_19 var_21_arg_0 = var_20; var_21_arg_0 = var_21_arg_0 & mask_SORT_19; SORT_13 var_21 = var_21_arg_0; SORT_13 var_22_arg_0 = var_14; SORT_13 var_22_arg_1 = var_21; SORT_1 var_22 = var_22_arg_0 == var_22_arg_1; SORT_13 var_16_arg_0 = var_14; SORT_13 var_16_arg_1 = var_15; SORT_1 var_16 = var_16_arg_0 == var_16_arg_1; SORT_1 var_17_arg_0 = var_16; SORT_3 var_17_arg_1 = state_10; SORT_3 var_17_arg_2 = input_9; SORT_3 var_17 = var_17_arg_0 ? var_17_arg_1 : var_17_arg_2; SORT_1 var_23_arg_0 = var_22; SORT_3 var_23_arg_1 = state_18; SORT_3 var_23_arg_2 = var_17; SORT_3 var_23 = var_23_arg_0 ? var_23_arg_1 : var_23_arg_2; SORT_1 var_28_arg_0 = var_27; SORT_3 var_28_arg_1 = state_24; SORT_3 var_28_arg_2 = var_23; SORT_3 var_28 = var_28_arg_0 ? var_28_arg_1 : var_28_arg_2; SORT_1 var_33_arg_0 = var_32; SORT_3 var_33_arg_1 = state_29; SORT_3 var_33_arg_2 = var_28; SORT_3 var_33 = var_33_arg_0 ? var_33_arg_1 : var_33_arg_2; SORT_1 var_38_arg_0 = var_37; SORT_3 var_38_arg_1 = state_34; SORT_3 var_38_arg_2 = var_33; SORT_3 var_38 = var_38_arg_0 ? var_38_arg_1 : var_38_arg_2; SORT_1 var_43_arg_0 = var_42; SORT_3 var_43_arg_1 = state_39; SORT_3 var_43_arg_2 = var_38; SORT_3 var_43 = var_43_arg_0 ? var_43_arg_1 : var_43_arg_2; SORT_1 var_48_arg_0 = var_47; SORT_3 var_48_arg_1 = state_44; SORT_3 var_48_arg_2 = var_43; SORT_3 var_48 = var_48_arg_0 ? var_48_arg_1 : var_48_arg_2; SORT_1 var_53_arg_0 = var_52; SORT_3 var_53_arg_1 = state_49; SORT_3 var_53_arg_2 = var_48; SORT_3 var_53 = var_53_arg_0 ? var_53_arg_1 : var_53_arg_2; SORT_1 var_58_arg_0 = var_57; SORT_3 var_58_arg_1 = state_54; SORT_3 var_58_arg_2 = var_53; SORT_3 var_58 = var_58_arg_0 ? var_58_arg_1 : var_58_arg_2; SORT_1 var_64_arg_0 = var_63; SORT_3 var_64_arg_1 = state_59; SORT_3 var_64_arg_2 = var_58; SORT_3 var_64 = var_64_arg_0 ? var_64_arg_1 : var_64_arg_2; SORT_1 var_69_arg_0 = var_68; SORT_3 var_69_arg_1 = state_65; SORT_3 var_69_arg_2 = var_64; SORT_3 var_69 = var_69_arg_0 ? var_69_arg_1 : var_69_arg_2; SORT_1 var_74_arg_0 = var_73; SORT_3 var_74_arg_1 = state_70; SORT_3 var_74_arg_2 = var_69; SORT_3 var_74 = var_74_arg_0 ? var_74_arg_1 : var_74_arg_2; SORT_1 var_79_arg_0 = var_78; SORT_3 var_79_arg_1 = state_75; SORT_3 var_79_arg_2 = var_74; SORT_3 var_79 = var_79_arg_0 ? var_79_arg_1 : var_79_arg_2; SORT_1 var_85_arg_0 = var_84; SORT_3 var_85_arg_1 = state_80; SORT_3 var_85_arg_2 = var_79; SORT_3 var_85 = var_85_arg_0 ? var_85_arg_1 : var_85_arg_2; SORT_1 var_90_arg_0 = var_89; SORT_3 var_90_arg_1 = state_86; SORT_3 var_90_arg_2 = var_85; SORT_3 var_90 = var_90_arg_0 ? var_90_arg_1 : var_90_arg_2; SORT_1 var_95_arg_0 = var_94; SORT_3 var_95_arg_1 = state_91; SORT_3 var_95_arg_2 = var_90; SORT_3 var_95 = var_95_arg_0 ? var_95_arg_1 : var_95_arg_2; SORT_1 var_99_arg_0 = var_98; SORT_3 var_99_arg_1 = state_96; SORT_3 var_99_arg_2 = var_95; SORT_3 var_99 = var_99_arg_0 ? var_99_arg_1 : var_99_arg_2; var_99 = var_99 & mask_SORT_3; SORT_3 var_129_arg_0 = state_128; SORT_3 var_129_arg_1 = var_99; SORT_1 var_129 = var_129_arg_0 == var_129_arg_1; SORT_1 var_130_arg_0 = var_127; SORT_1 var_130_arg_1 = var_129; SORT_1 var_130 = var_130_arg_0 | var_130_arg_1; SORT_1 var_151_arg_0 = state_132; SORT_1 var_151_arg_1 = input_150; SORT_1 var_151_arg_2 = var_130; SORT_1 var_151 = var_151_arg_0 ? var_151_arg_1 : var_151_arg_2; SORT_1 var_154_arg_0 = var_151; SORT_1 var_154 = ~var_154_arg_0; SORT_1 var_155_arg_0 = var_153; SORT_1 var_155_arg_1 = var_154; SORT_1 var_155 = var_155_arg_0 & var_155_arg_1; var_155 = var_155 & mask_SORT_1; SORT_1 bad_156_arg_0 = var_155; __VERIFIER_assert(!(bad_156_arg_0)); // Computing next states ... SORT_11 var_186_arg_0 = state_185; SORT_13 var_186 = var_186_arg_0 >> 0; var_186 = var_186 & mask_SORT_13; SORT_13 var_236_arg_0 = var_186; SORT_13 var_236_arg_1 = var_15; SORT_1 var_236 = var_236_arg_0 == var_236_arg_1; SORT_1 var_237_arg_0 = input_6; SORT_1 var_237_arg_1 = var_236; SORT_1 var_237 = var_237_arg_0 & var_237_arg_1; var_237 = var_237 & mask_SORT_1; SORT_1 var_372_arg_0 = var_237; SORT_3 var_372_arg_1 = input_4; SORT_3 var_372_arg_2 = state_10; SORT_3 var_372 = var_372_arg_0 ? var_372_arg_1 : var_372_arg_2; SORT_1 var_374_arg_0 = input_7; SORT_3 var_374_arg_1 = var_373; SORT_3 var_374_arg_2 = var_372; SORT_3 var_374 = var_374_arg_0 ? var_374_arg_1 : var_374_arg_2; SORT_3 next_375_arg_1 = var_374; SORT_1 var_160_arg_0 = input_6; SORT_1 var_160_arg_1 = input_5; SORT_1 var_160 = var_160_arg_0 | var_160_arg_1; SORT_1 var_161_arg_0 = var_160; SORT_1 var_161_arg_1 = input_7; SORT_1 var_161 = var_161_arg_0 | var_161_arg_1; var_161 = var_161 & mask_SORT_1; SORT_1 var_303_arg_0 = input_5; var_303_arg_0 = var_303_arg_0 & mask_SORT_1; SORT_11 var_303 = var_303_arg_0; SORT_11 var_304_arg_0 = state_12; SORT_11 var_304_arg_1 = var_303; SORT_11 var_304 = var_304_arg_0 + var_304_arg_1; SORT_1 var_376_arg_0 = var_161; SORT_11 var_376_arg_1 = var_304; SORT_11 var_376_arg_2 = state_12; SORT_11 var_376 = var_376_arg_0 ? var_376_arg_1 : var_376_arg_2; SORT_1 var_377_arg_0 = input_7; SORT_11 var_377_arg_1 = var_122; SORT_11 var_377_arg_2 = var_376; SORT_11 var_377 = var_377_arg_0 ? var_377_arg_1 : var_377_arg_2; SORT_11 next_378_arg_1 = var_377; SORT_19 var_229_arg_0 = var_20; var_229_arg_0 = var_229_arg_0 & mask_SORT_19; SORT_13 var_229 = var_229_arg_0; SORT_13 var_230_arg_0 = var_186; SORT_13 var_230_arg_1 = var_229; SORT_1 var_230 = var_230_arg_0 == var_230_arg_1; SORT_1 var_231_arg_0 = input_6; SORT_1 var_231_arg_1 = var_230; SORT_1 var_231 = var_231_arg_0 & var_231_arg_1; var_231 = var_231 & mask_SORT_1; SORT_1 var_379_arg_0 = var_231; SORT_3 var_379_arg_1 = input_4; SORT_3 var_379_arg_2 = state_18; SORT_3 var_379 = var_379_arg_0 ? var_379_arg_1 : var_379_arg_2; SORT_1 var_380_arg_0 = input_7; SORT_3 var_380_arg_1 = var_373; SORT_3 var_380_arg_2 = var_379; SORT_3 var_380 = var_380_arg_0 ? var_380_arg_1 : var_380_arg_2; SORT_3 next_381_arg_1 = var_380; SORT_19 var_222_arg_0 = var_25; var_222_arg_0 = var_222_arg_0 & mask_SORT_19; SORT_13 var_222 = var_222_arg_0; SORT_13 var_223_arg_0 = var_186; SORT_13 var_223_arg_1 = var_222; SORT_1 var_223 = var_223_arg_0 == var_223_arg_1; SORT_1 var_224_arg_0 = input_6; SORT_1 var_224_arg_1 = var_223; SORT_1 var_224 = var_224_arg_0 & var_224_arg_1; var_224 = var_224 & mask_SORT_1; SORT_1 var_382_arg_0 = var_224; SORT_3 var_382_arg_1 = input_4; SORT_3 var_382_arg_2 = state_24; SORT_3 var_382 = var_382_arg_0 ? var_382_arg_1 : var_382_arg_2; SORT_1 var_383_arg_0 = input_7; SORT_3 var_383_arg_1 = var_373; SORT_3 var_383_arg_2 = var_382; SORT_3 var_383 = var_383_arg_0 ? var_383_arg_1 : var_383_arg_2; SORT_3 next_384_arg_1 = var_383; SORT_19 var_215_arg_0 = var_30; var_215_arg_0 = var_215_arg_0 & mask_SORT_19; SORT_13 var_215 = var_215_arg_0; SORT_13 var_216_arg_0 = var_186; SORT_13 var_216_arg_1 = var_215; SORT_1 var_216 = var_216_arg_0 == var_216_arg_1; SORT_1 var_217_arg_0 = input_6; SORT_1 var_217_arg_1 = var_216; SORT_1 var_217 = var_217_arg_0 & var_217_arg_1; var_217 = var_217 & mask_SORT_1; SORT_1 var_385_arg_0 = var_217; SORT_3 var_385_arg_1 = input_4; SORT_3 var_385_arg_2 = state_29; SORT_3 var_385 = var_385_arg_0 ? var_385_arg_1 : var_385_arg_2; SORT_1 var_386_arg_0 = input_7; SORT_3 var_386_arg_1 = var_373; SORT_3 var_386_arg_2 = var_385; SORT_3 var_386 = var_386_arg_0 ? var_386_arg_1 : var_386_arg_2; SORT_3 next_387_arg_1 = var_386; SORT_19 var_208_arg_0 = var_35; var_208_arg_0 = var_208_arg_0 & mask_SORT_19; SORT_13 var_208 = var_208_arg_0; SORT_13 var_209_arg_0 = var_186; SORT_13 var_209_arg_1 = var_208; SORT_1 var_209 = var_209_arg_0 == var_209_arg_1; SORT_1 var_210_arg_0 = input_6; SORT_1 var_210_arg_1 = var_209; SORT_1 var_210 = var_210_arg_0 & var_210_arg_1; var_210 = var_210 & mask_SORT_1; SORT_1 var_388_arg_0 = var_210; SORT_3 var_388_arg_1 = input_4; SORT_3 var_388_arg_2 = state_34; SORT_3 var_388 = var_388_arg_0 ? var_388_arg_1 : var_388_arg_2; SORT_1 var_389_arg_0 = input_7; SORT_3 var_389_arg_1 = var_373; SORT_3 var_389_arg_2 = var_388; SORT_3 var_389 = var_389_arg_0 ? var_389_arg_1 : var_389_arg_2; SORT_3 next_390_arg_1 = var_389; SORT_19 var_201_arg_0 = var_40; var_201_arg_0 = var_201_arg_0 & mask_SORT_19; SORT_13 var_201 = var_201_arg_0; SORT_13 var_202_arg_0 = var_186; SORT_13 var_202_arg_1 = var_201; SORT_1 var_202 = var_202_arg_0 == var_202_arg_1; SORT_1 var_203_arg_0 = input_6; SORT_1 var_203_arg_1 = var_202; SORT_1 var_203 = var_203_arg_0 & var_203_arg_1; var_203 = var_203 & mask_SORT_1; SORT_1 var_391_arg_0 = var_203; SORT_3 var_391_arg_1 = input_4; SORT_3 var_391_arg_2 = state_39; SORT_3 var_391 = var_391_arg_0 ? var_391_arg_1 : var_391_arg_2; SORT_1 var_392_arg_0 = input_7; SORT_3 var_392_arg_1 = var_373; SORT_3 var_392_arg_2 = var_391; SORT_3 var_392 = var_392_arg_0 ? var_392_arg_1 : var_392_arg_2; SORT_3 next_393_arg_1 = var_392; SORT_19 var_194_arg_0 = var_45; var_194_arg_0 = var_194_arg_0 & mask_SORT_19; SORT_13 var_194 = var_194_arg_0; SORT_13 var_195_arg_0 = var_186; SORT_13 var_195_arg_1 = var_194; SORT_1 var_195 = var_195_arg_0 == var_195_arg_1; SORT_1 var_196_arg_0 = input_6; SORT_1 var_196_arg_1 = var_195; SORT_1 var_196 = var_196_arg_0 & var_196_arg_1; var_196 = var_196 & mask_SORT_1; SORT_1 var_394_arg_0 = var_196; SORT_3 var_394_arg_1 = input_4; SORT_3 var_394_arg_2 = state_44; SORT_3 var_394 = var_394_arg_0 ? var_394_arg_1 : var_394_arg_2; SORT_1 var_395_arg_0 = input_7; SORT_3 var_395_arg_1 = var_373; SORT_3 var_395_arg_2 = var_394; SORT_3 var_395 = var_395_arg_0 ? var_395_arg_1 : var_395_arg_2; SORT_3 next_396_arg_1 = var_395; SORT_19 var_298_arg_0 = var_50; var_298_arg_0 = var_298_arg_0 & mask_SORT_19; SORT_13 var_298 = var_298_arg_0; SORT_13 var_299_arg_0 = var_186; SORT_13 var_299_arg_1 = var_298; SORT_1 var_299 = var_299_arg_0 == var_299_arg_1; SORT_1 var_300_arg_0 = input_6; SORT_1 var_300_arg_1 = var_299; SORT_1 var_300 = var_300_arg_0 & var_300_arg_1; var_300 = var_300 & mask_SORT_1; SORT_1 var_397_arg_0 = var_300; SORT_3 var_397_arg_1 = input_4; SORT_3 var_397_arg_2 = state_49; SORT_3 var_397 = var_397_arg_0 ? var_397_arg_1 : var_397_arg_2; SORT_1 var_398_arg_0 = input_7; SORT_3 var_398_arg_1 = var_373; SORT_3 var_398_arg_2 = var_397; SORT_3 var_398 = var_398_arg_0 ? var_398_arg_1 : var_398_arg_2; SORT_3 next_399_arg_1 = var_398; SORT_19 var_291_arg_0 = var_55; var_291_arg_0 = var_291_arg_0 & mask_SORT_19; SORT_13 var_291 = var_291_arg_0; SORT_13 var_292_arg_0 = var_186; SORT_13 var_292_arg_1 = var_291; SORT_1 var_292 = var_292_arg_0 == var_292_arg_1; SORT_1 var_293_arg_0 = input_6; SORT_1 var_293_arg_1 = var_292; SORT_1 var_293 = var_293_arg_0 & var_293_arg_1; var_293 = var_293 & mask_SORT_1; SORT_1 var_400_arg_0 = var_293; SORT_3 var_400_arg_1 = input_4; SORT_3 var_400_arg_2 = state_54; SORT_3 var_400 = var_400_arg_0 ? var_400_arg_1 : var_400_arg_2; SORT_1 var_401_arg_0 = input_7; SORT_3 var_401_arg_1 = var_373; SORT_3 var_401_arg_2 = var_400; SORT_3 var_401 = var_401_arg_0 ? var_401_arg_1 : var_401_arg_2; SORT_3 next_402_arg_1 = var_401; SORT_60 var_284_arg_0 = var_61; var_284_arg_0 = var_284_arg_0 & mask_SORT_60; SORT_13 var_284 = var_284_arg_0; SORT_13 var_285_arg_0 = var_186; SORT_13 var_285_arg_1 = var_284; SORT_1 var_285 = var_285_arg_0 == var_285_arg_1; SORT_1 var_286_arg_0 = input_6; SORT_1 var_286_arg_1 = var_285; SORT_1 var_286 = var_286_arg_0 & var_286_arg_1; var_286 = var_286 & mask_SORT_1; SORT_1 var_403_arg_0 = var_286; SORT_3 var_403_arg_1 = input_4; SORT_3 var_403_arg_2 = state_59; SORT_3 var_403 = var_403_arg_0 ? var_403_arg_1 : var_403_arg_2; SORT_1 var_404_arg_0 = input_7; SORT_3 var_404_arg_1 = var_373; SORT_3 var_404_arg_2 = var_403; SORT_3 var_404 = var_404_arg_0 ? var_404_arg_1 : var_404_arg_2; SORT_3 next_405_arg_1 = var_404; SORT_60 var_277_arg_0 = var_66; var_277_arg_0 = var_277_arg_0 & mask_SORT_60; SORT_13 var_277 = var_277_arg_0; SORT_13 var_278_arg_0 = var_186; SORT_13 var_278_arg_1 = var_277; SORT_1 var_278 = var_278_arg_0 == var_278_arg_1; SORT_1 var_279_arg_0 = input_6; SORT_1 var_279_arg_1 = var_278; SORT_1 var_279 = var_279_arg_0 & var_279_arg_1; var_279 = var_279 & mask_SORT_1; SORT_1 var_406_arg_0 = var_279; SORT_3 var_406_arg_1 = input_4; SORT_3 var_406_arg_2 = state_65; SORT_3 var_406 = var_406_arg_0 ? var_406_arg_1 : var_406_arg_2; SORT_1 var_407_arg_0 = input_7; SORT_3 var_407_arg_1 = var_373; SORT_3 var_407_arg_2 = var_406; SORT_3 var_407 = var_407_arg_0 ? var_407_arg_1 : var_407_arg_2; SORT_3 next_408_arg_1 = var_407; SORT_60 var_270_arg_0 = var_71; var_270_arg_0 = var_270_arg_0 & mask_SORT_60; SORT_13 var_270 = var_270_arg_0; SORT_13 var_271_arg_0 = var_186; SORT_13 var_271_arg_1 = var_270; SORT_1 var_271 = var_271_arg_0 == var_271_arg_1; SORT_1 var_272_arg_0 = input_6; SORT_1 var_272_arg_1 = var_271; SORT_1 var_272 = var_272_arg_0 & var_272_arg_1; var_272 = var_272 & mask_SORT_1; SORT_1 var_409_arg_0 = var_272; SORT_3 var_409_arg_1 = input_4; SORT_3 var_409_arg_2 = state_70; SORT_3 var_409 = var_409_arg_0 ? var_409_arg_1 : var_409_arg_2; SORT_1 var_410_arg_0 = input_7; SORT_3 var_410_arg_1 = var_373; SORT_3 var_410_arg_2 = var_409; SORT_3 var_410 = var_410_arg_0 ? var_410_arg_1 : var_410_arg_2; SORT_3 next_411_arg_1 = var_410; SORT_60 var_263_arg_0 = var_76; var_263_arg_0 = var_263_arg_0 & mask_SORT_60; SORT_13 var_263 = var_263_arg_0; SORT_13 var_264_arg_0 = var_186; SORT_13 var_264_arg_1 = var_263; SORT_1 var_264 = var_264_arg_0 == var_264_arg_1; SORT_1 var_265_arg_0 = input_6; SORT_1 var_265_arg_1 = var_264; SORT_1 var_265 = var_265_arg_0 & var_265_arg_1; var_265 = var_265 & mask_SORT_1; SORT_1 var_412_arg_0 = var_265; SORT_3 var_412_arg_1 = input_4; SORT_3 var_412_arg_2 = state_75; SORT_3 var_412 = var_412_arg_0 ? var_412_arg_1 : var_412_arg_2; SORT_1 var_413_arg_0 = input_7; SORT_3 var_413_arg_1 = var_373; SORT_3 var_413_arg_2 = var_412; SORT_3 var_413 = var_413_arg_0 ? var_413_arg_1 : var_413_arg_2; SORT_3 next_414_arg_1 = var_413; SORT_81 var_256_arg_0 = var_82; var_256_arg_0 = var_256_arg_0 & mask_SORT_81; SORT_13 var_256 = var_256_arg_0; SORT_13 var_257_arg_0 = var_186; SORT_13 var_257_arg_1 = var_256; SORT_1 var_257 = var_257_arg_0 == var_257_arg_1; SORT_1 var_258_arg_0 = input_6; SORT_1 var_258_arg_1 = var_257; SORT_1 var_258 = var_258_arg_0 & var_258_arg_1; var_258 = var_258 & mask_SORT_1; SORT_1 var_415_arg_0 = var_258; SORT_3 var_415_arg_1 = input_4; SORT_3 var_415_arg_2 = state_80; SORT_3 var_415 = var_415_arg_0 ? var_415_arg_1 : var_415_arg_2; SORT_1 var_416_arg_0 = input_7; SORT_3 var_416_arg_1 = var_373; SORT_3 var_416_arg_2 = var_415; SORT_3 var_416 = var_416_arg_0 ? var_416_arg_1 : var_416_arg_2; SORT_3 next_417_arg_1 = var_416; SORT_81 var_249_arg_0 = var_87; var_249_arg_0 = var_249_arg_0 & mask_SORT_81; SORT_13 var_249 = var_249_arg_0; SORT_13 var_250_arg_0 = var_186; SORT_13 var_250_arg_1 = var_249; SORT_1 var_250 = var_250_arg_0 == var_250_arg_1; SORT_1 var_251_arg_0 = input_6; SORT_1 var_251_arg_1 = var_250; SORT_1 var_251 = var_251_arg_0 & var_251_arg_1; var_251 = var_251 & mask_SORT_1; SORT_1 var_418_arg_0 = var_251; SORT_3 var_418_arg_1 = input_4; SORT_3 var_418_arg_2 = state_86; SORT_3 var_418 = var_418_arg_0 ? var_418_arg_1 : var_418_arg_2; SORT_1 var_419_arg_0 = input_7; SORT_3 var_419_arg_1 = var_373; SORT_3 var_419_arg_2 = var_418; SORT_3 var_419 = var_419_arg_0 ? var_419_arg_1 : var_419_arg_2; SORT_3 next_420_arg_1 = var_419; SORT_1 var_242_arg_0 = var_92; var_242_arg_0 = var_242_arg_0 & mask_SORT_1; SORT_13 var_242 = var_242_arg_0; SORT_13 var_243_arg_0 = var_186; SORT_13 var_243_arg_1 = var_242; SORT_1 var_243 = var_243_arg_0 == var_243_arg_1; SORT_1 var_244_arg_0 = input_6; SORT_1 var_244_arg_1 = var_243; SORT_1 var_244 = var_244_arg_0 & var_244_arg_1; var_244 = var_244 & mask_SORT_1; SORT_1 var_421_arg_0 = var_244; SORT_3 var_421_arg_1 = input_4; SORT_3 var_421_arg_2 = state_91; SORT_3 var_421 = var_421_arg_0 ? var_421_arg_1 : var_421_arg_2; SORT_1 var_422_arg_0 = input_7; SORT_3 var_422_arg_1 = var_373; SORT_3 var_422_arg_2 = var_421; SORT_3 var_422 = var_422_arg_0 ? var_422_arg_1 : var_422_arg_2; SORT_3 next_423_arg_1 = var_422; SORT_13 var_187_arg_0 = var_186; SORT_1 var_187 = var_187_arg_0 != 0; SORT_1 var_188_arg_0 = var_187; SORT_1 var_188 = ~var_188_arg_0; SORT_1 var_189_arg_0 = input_6; SORT_1 var_189_arg_1 = var_188; SORT_1 var_189 = var_189_arg_0 & var_189_arg_1; var_189 = var_189 & mask_SORT_1; SORT_1 var_424_arg_0 = var_189; SORT_3 var_424_arg_1 = input_4; SORT_3 var_424_arg_2 = state_96; SORT_3 var_424 = var_424_arg_0 ? var_424_arg_1 : var_424_arg_2; SORT_1 var_425_arg_0 = input_7; SORT_3 var_425_arg_1 = var_373; SORT_3 var_425_arg_2 = var_424; SORT_3 var_425 = var_425_arg_0 ? var_425_arg_1 : var_425_arg_2; SORT_3 next_426_arg_1 = var_425; SORT_1 var_427_arg_0 = input_6; var_427_arg_0 = var_427_arg_0 & mask_SORT_1; SORT_11 var_427 = var_427_arg_0; SORT_11 var_428_arg_0 = state_101; SORT_11 var_428_arg_1 = var_427; SORT_11 var_428 = var_428_arg_0 + var_428_arg_1; SORT_1 var_429_arg_0 = input_5; var_429_arg_0 = var_429_arg_0 & mask_SORT_1; SORT_11 var_429 = var_429_arg_0; SORT_11 var_430_arg_0 = var_428; SORT_11 var_430_arg_1 = var_429; SORT_11 var_430 = var_430_arg_0 - var_430_arg_1; SORT_1 var_431_arg_0 = input_7; SORT_11 var_431_arg_1 = var_122; SORT_11 var_431_arg_2 = var_430; SORT_11 var_431 = var_431_arg_0 ? var_431_arg_1 : var_431_arg_2; var_431 = var_431 & mask_SORT_11; SORT_11 next_432_arg_1 = var_431; SORT_1 var_333_arg_0 = state_109; SORT_1 var_333 = ~var_333_arg_0; var_333 = var_333 & mask_SORT_1; SORT_1 var_329_arg_0 = input_8; SORT_1 var_329_arg_1 = input_6; SORT_1 var_329 = var_329_arg_0 & var_329_arg_1; SORT_1 var_330_arg_0 = state_109; SORT_1 var_330_arg_1 = var_329; SORT_1 var_330 = var_330_arg_0 | var_330_arg_1; SORT_1 var_433_arg_0 = var_333; SORT_1 var_433_arg_1 = var_330; SORT_1 var_433_arg_2 = state_109; SORT_1 var_433 = var_433_arg_0 ? var_433_arg_1 : var_433_arg_2; SORT_1 var_434_arg_0 = input_7; SORT_1 var_434_arg_1 = var_152; SORT_1 var_434_arg_2 = var_433; SORT_1 var_434 = var_434_arg_0 ? var_434_arg_1 : var_434_arg_2; SORT_1 next_435_arg_1 = var_434; SORT_1 var_341_arg_0 = var_126; SORT_1 var_341_arg_1 = state_110; SORT_1 var_341 = var_341_arg_0 | var_341_arg_1; SORT_1 var_436_arg_0 = var_92; SORT_1 var_436_arg_1 = var_341; SORT_1 var_436_arg_2 = state_110; SORT_1 var_436 = var_436_arg_0 ? var_436_arg_1 : var_436_arg_2; SORT_1 var_437_arg_0 = input_7; SORT_1 var_437_arg_1 = var_152; SORT_1 var_437_arg_2 = var_436; SORT_1 var_437 = var_437_arg_0 ? var_437_arg_1 : var_437_arg_2; SORT_1 next_438_arg_1 = var_437; SORT_1 var_353_arg_0 = input_6; SORT_1 var_353_arg_1 = input_5; SORT_1 var_353 = var_353_arg_0 | var_353_arg_1; SORT_1 var_354_arg_0 = var_353; SORT_1 var_354_arg_1 = input_7; SORT_1 var_354 = var_354_arg_0 | var_354_arg_1; SORT_1 var_355_arg_0 = var_354; SORT_1 var_355_arg_1 = state_109; SORT_1 var_355 = var_355_arg_0 | var_355_arg_1; var_355 = var_355 & mask_SORT_1; SORT_1 var_439_arg_0 = var_355; SORT_11 var_439_arg_1 = var_123; SORT_11 var_439_arg_2 = state_113; SORT_11 var_439 = var_439_arg_0 ? var_439_arg_1 : var_439_arg_2; SORT_1 var_440_arg_0 = input_7; SORT_11 var_440_arg_1 = var_122; SORT_11 var_440_arg_2 = var_439; SORT_11 var_440 = var_440_arg_0 ? var_440_arg_1 : var_440_arg_2; var_440 = var_440 & mask_SORT_11; SORT_11 next_441_arg_1 = var_440; SORT_1 var_338_arg_0 = var_329; SORT_1 var_338_arg_1 = var_333; SORT_1 var_338 = var_338_arg_0 & var_338_arg_1; var_338 = var_338 & mask_SORT_1; SORT_1 var_442_arg_0 = var_338; SORT_3 var_442_arg_1 = input_4; SORT_3 var_442_arg_2 = state_128; SORT_3 var_442 = var_442_arg_0 ? var_442_arg_1 : var_442_arg_2; SORT_1 var_443_arg_0 = input_7; SORT_3 var_443_arg_1 = var_373; SORT_3 var_443_arg_2 = var_442; SORT_3 var_443 = var_443_arg_0 ? var_443_arg_1 : var_443_arg_2; var_443 = var_443 & mask_SORT_3; SORT_3 next_444_arg_1 = var_443; SORT_1 next_445_arg_1 = var_152; SORT_1 var_309_arg_0 = input_6; var_309_arg_0 = var_309_arg_0 & mask_SORT_1; SORT_11 var_309 = var_309_arg_0; SORT_11 var_310_arg_0 = state_185; SORT_11 var_310_arg_1 = var_309; SORT_11 var_310 = var_310_arg_0 + var_310_arg_1; SORT_1 var_446_arg_0 = var_161; SORT_11 var_446_arg_1 = var_310; SORT_11 var_446_arg_2 = state_185; SORT_11 var_446 = var_446_arg_0 ? var_446_arg_1 : var_446_arg_2; SORT_1 var_447_arg_0 = input_7; SORT_11 var_447_arg_1 = var_122; SORT_11 var_447_arg_2 = var_446; SORT_11 var_447 = var_447_arg_0 ? var_447_arg_1 : var_447_arg_2; SORT_11 next_448_arg_1 = var_447; // Assigning next states ... state_10 = next_375_arg_1; state_12 = next_378_arg_1; state_18 = next_381_arg_1; state_24 = next_384_arg_1; state_29 = next_387_arg_1; state_34 = next_390_arg_1; state_39 = next_393_arg_1; state_44 = next_396_arg_1; state_49 = next_399_arg_1; state_54 = next_402_arg_1; state_59 = next_405_arg_1; state_65 = next_408_arg_1; state_70 = next_411_arg_1; state_75 = next_414_arg_1; state_80 = next_417_arg_1; state_86 = next_420_arg_1; state_91 = next_423_arg_1; state_96 = next_426_arg_1; state_101 = next_432_arg_1; state_109 = next_435_arg_1; state_110 = next_438_arg_1; state_113 = next_441_arg_1; state_128 = next_444_arg_1; state_132 = next_445_arg_1; state_185 = next_448_arg_1; } return 0; }