// 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=false, 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_w8_d8_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 char SORT_3; // BV with 8 bits const SORT_3 mask_SORT_3 = (SORT_3)-1 >> (sizeof(SORT_3) * 8 - 8); const SORT_3 msb_SORT_3 = (SORT_3)1 << (8 - 1); typedef unsigned char SORT_11; // BV with 5 bits const SORT_11 mask_SORT_11 = (SORT_11)-1 >> (sizeof(SORT_11) * 8 - 5); const SORT_11 msb_SORT_11 = (SORT_11)1 << (5 - 1); typedef unsigned char SORT_13; // BV with 4 bits const SORT_13 mask_SORT_13 = (SORT_13)-1 >> (sizeof(SORT_13) * 8 - 4); const SORT_13 msb_SORT_13 = (SORT_13)1 << (4 - 1); typedef unsigned char SORT_19; // BV with 3 bits const SORT_19 mask_SORT_19 = (SORT_19)-1 >> (sizeof(SORT_19) * 8 - 3); const SORT_19 msb_SORT_19 = (SORT_19)1 << (3 - 1); typedef unsigned char SORT_40; // BV with 2 bits const SORT_40 mask_SORT_40 = (SORT_40)-1 >> (sizeof(SORT_40) * 8 - 2); const SORT_40 msb_SORT_40 = (SORT_40)1 << (2 - 1); // Initializing constants ... const SORT_13 var_15 = 8; const SORT_19 var_20 = 7; const SORT_19 var_25 = 6; const SORT_19 var_30 = 5; const SORT_19 var_35 = 4; const SORT_40 var_41 = 3; const SORT_40 var_46 = 2; const SORT_1 var_51 = 1; const SORT_13 var_64 = 9; const SORT_11 var_81 = 0; const SORT_1 var_111 = 0; const SORT_3 var_268 = 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_109; // Collecting state declarations ... SORT_3 state_10 = __VERIFIER_nondet_uchar() & mask_SORT_3; SORT_11 state_12 = __VERIFIER_nondet_uchar() & mask_SORT_11; SORT_3 state_18 = __VERIFIER_nondet_uchar() & mask_SORT_3; SORT_3 state_24 = __VERIFIER_nondet_uchar() & mask_SORT_3; SORT_3 state_29 = __VERIFIER_nondet_uchar() & mask_SORT_3; SORT_3 state_34 = __VERIFIER_nondet_uchar() & mask_SORT_3; SORT_3 state_39 = __VERIFIER_nondet_uchar() & mask_SORT_3; SORT_3 state_45 = __VERIFIER_nondet_uchar() & mask_SORT_3; SORT_3 state_50 = __VERIFIER_nondet_uchar() & mask_SORT_3; SORT_3 state_55 = __VERIFIER_nondet_uchar() & mask_SORT_3; SORT_11 state_60 = __VERIFIER_nondet_uchar() & mask_SORT_11; SORT_1 state_68 = __VERIFIER_nondet_uchar() & mask_SORT_1; SORT_1 state_69 = __VERIFIER_nondet_uchar() & mask_SORT_1; SORT_11 state_72 = __VERIFIER_nondet_uchar() & mask_SORT_11; SORT_3 state_87 = __VERIFIER_nondet_uchar() & mask_SORT_3; SORT_1 state_91 = __VERIFIER_nondet_uchar() & mask_SORT_1; SORT_11 state_136 = __VERIFIER_nondet_uchar() & mask_SORT_11; // Initializing states ... SORT_1 init_92_arg_1 = var_51; state_91 = init_92_arg_1; for (;;) { // Getting external input values ... input_2 = __VERIFIER_nondet_uchar(); input_2 = input_2 & mask_SORT_1; input_4 = __VERIFIER_nondet_uchar(); input_4 = input_4 & mask_SORT_3; input_5 = __VERIFIER_nondet_uchar(); input_5 = input_5 & mask_SORT_1; input_6 = __VERIFIER_nondet_uchar(); input_6 = input_6 & mask_SORT_1; input_7 = __VERIFIER_nondet_uchar(); input_7 = input_7 & mask_SORT_1; input_8 = __VERIFIER_nondet_uchar(); input_8 = input_8 & mask_SORT_1; input_9 = __VERIFIER_nondet_uchar(); input_9 = input_9 & mask_SORT_3; input_109 = __VERIFIER_nondet_uchar(); input_109 = input_109 & mask_SORT_1; // Assuming invariants ... SORT_1 var_93_arg_0 = input_7; SORT_1 var_93_arg_1 = state_91; SORT_1 var_93 = var_93_arg_0 == var_93_arg_1; SORT_1 var_94_arg_0 = var_51; SORT_1 var_94 = ~var_94_arg_0; var_94 = var_94 & mask_SORT_1; SORT_1 var_95_arg_0 = var_93; SORT_1 var_95_arg_1 = var_94; SORT_1 var_95 = var_95_arg_0 | var_95_arg_1; var_95 = var_95 & mask_SORT_1; SORT_1 constr_96_arg_0 = var_95; assume_abort_if_not(constr_96_arg_0); SORT_13 var_65_arg_0 = var_64; SORT_11 var_65 = var_65_arg_0; SORT_11 var_66_arg_0 = state_60; SORT_11 var_66_arg_1 = var_65; SORT_1 var_66 = var_66_arg_0 == var_66_arg_1; SORT_1 var_97_arg_0 = var_66; SORT_1 var_97 = ~var_97_arg_0; var_97 = var_97 & mask_SORT_1; SORT_1 var_98_arg_0 = input_6; SORT_1 var_98 = ~var_98_arg_0; var_98 = var_98 & mask_SORT_1; SORT_1 var_99_arg_0 = var_97; SORT_1 var_99_arg_1 = var_98; SORT_1 var_99 = var_99_arg_0 | var_99_arg_1; var_99 = var_99 & mask_SORT_1; SORT_1 var_100_arg_0 = var_51; SORT_1 var_100 = ~var_100_arg_0; var_100 = var_100 & mask_SORT_1; SORT_1 var_101_arg_0 = var_99; SORT_1 var_101_arg_1 = var_100; SORT_1 var_101 = var_101_arg_0 | var_101_arg_1; var_101 = var_101 & mask_SORT_1; SORT_1 constr_102_arg_0 = var_101; assume_abort_if_not(constr_102_arg_0); SORT_11 var_61_arg_0 = state_60; SORT_1 var_61 = var_61_arg_0 != 0; SORT_1 var_62_arg_0 = var_61; SORT_1 var_62 = ~var_62_arg_0; var_62 = var_62 & mask_SORT_1; SORT_1 var_103_arg_0 = var_62; SORT_1 var_103 = ~var_103_arg_0; var_103 = var_103 & mask_SORT_1; SORT_1 var_104_arg_0 = input_5; SORT_1 var_104 = ~var_104_arg_0; var_104 = var_104 & mask_SORT_1; SORT_1 var_105_arg_0 = var_103; SORT_1 var_105_arg_1 = var_104; SORT_1 var_105 = var_105_arg_0 | var_105_arg_1; var_105 = var_105 & mask_SORT_1; SORT_1 var_106_arg_0 = var_51; SORT_1 var_106 = ~var_106_arg_0; var_106 = var_106 & mask_SORT_1; SORT_1 var_107_arg_0 = var_105; SORT_1 var_107_arg_1 = var_106; SORT_1 var_107 = var_107_arg_0 | var_107_arg_1; var_107 = var_107 & mask_SORT_1; SORT_1 constr_108_arg_0 = var_107; assume_abort_if_not(constr_108_arg_0); // Asserting properties ... SORT_1 var_112_arg_0 = state_91; SORT_1 var_112_arg_1 = var_111; SORT_1 var_112_arg_2 = var_51; SORT_1 var_112 = var_112_arg_0 ? var_112_arg_1 : var_112_arg_2; SORT_1 var_70_arg_0 = state_69; SORT_1 var_70 = ~var_70_arg_0; var_70 = var_70 & mask_SORT_1; SORT_1 var_71_arg_0 = state_68; SORT_1 var_71_arg_1 = var_70; SORT_1 var_71 = var_71_arg_0 & var_71_arg_1; var_71 = var_71 & mask_SORT_1; SORT_11 var_73_arg_0 = state_72; SORT_1 var_73 = var_73_arg_0 != 0; SORT_1 var_74_arg_0 = var_71; SORT_1 var_74_arg_1 = var_73; SORT_1 var_74 = var_74_arg_0 & var_74_arg_1; var_74 = var_74 & mask_SORT_1; SORT_1 var_75_arg_0 = state_68; SORT_1 var_75 = ~var_75_arg_0; var_75 = var_75 & mask_SORT_1; SORT_1 var_76_arg_0 = input_6; SORT_1 var_76_arg_1 = var_75; SORT_1 var_76 = var_76_arg_0 & var_76_arg_1; var_76 = var_76 & mask_SORT_1; SORT_1 var_77_arg_0 = var_76; SORT_11 var_77 = var_77_arg_0; SORT_11 var_78_arg_0 = state_72; SORT_11 var_78_arg_1 = var_77; SORT_11 var_78 = var_78_arg_0 + var_78_arg_1; var_78 = var_78 & mask_SORT_11; SORT_1 var_79_arg_0 = input_5; SORT_11 var_79 = var_79_arg_0; SORT_11 var_80_arg_0 = var_78; SORT_11 var_80_arg_1 = var_79; SORT_11 var_80 = var_80_arg_0 - var_80_arg_1; var_80 = var_80 & mask_SORT_11; SORT_1 var_82_arg_0 = input_7; SORT_11 var_82_arg_1 = var_81; SORT_11 var_82_arg_2 = var_80; SORT_11 var_82 = var_82_arg_0 ? var_82_arg_1 : var_82_arg_2; SORT_11 var_83_arg_0 = var_82; SORT_1 var_83 = var_83_arg_0 != 0; SORT_1 var_84_arg_0 = var_83; SORT_1 var_84 = ~var_84_arg_0; var_84 = var_84 & mask_SORT_1; SORT_1 var_85_arg_0 = var_74; SORT_1 var_85_arg_1 = var_84; SORT_1 var_85 = var_85_arg_0 & var_85_arg_1; var_85 = var_85 & mask_SORT_1; SORT_1 var_86_arg_0 = var_85; SORT_1 var_86 = ~var_86_arg_0; var_86 = var_86 & mask_SORT_1; 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_56_arg_0 = var_14; SORT_1 var_56 = var_56_arg_0 != 0; SORT_1 var_57_arg_0 = var_56; SORT_1 var_57 = ~var_57_arg_0; var_57 = var_57 & mask_SORT_1; SORT_1 var_52_arg_0 = var_51; SORT_13 var_52 = var_52_arg_0; SORT_13 var_53_arg_0 = var_14; SORT_13 var_53_arg_1 = var_52; SORT_1 var_53 = var_53_arg_0 == var_53_arg_1; SORT_40 var_47_arg_0 = var_46; SORT_13 var_47 = var_47_arg_0; SORT_13 var_48_arg_0 = var_14; SORT_13 var_48_arg_1 = var_47; SORT_1 var_48 = var_48_arg_0 == var_48_arg_1; SORT_40 var_42_arg_0 = var_41; SORT_13 var_42 = var_42_arg_0; SORT_13 var_43_arg_0 = var_14; SORT_13 var_43_arg_1 = var_42; SORT_1 var_43 = var_43_arg_0 == var_43_arg_1; SORT_19 var_36_arg_0 = var_35; 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; 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; 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; 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_44_arg_0 = var_43; SORT_3 var_44_arg_1 = state_39; SORT_3 var_44_arg_2 = var_38; SORT_3 var_44 = var_44_arg_0 ? var_44_arg_1 : var_44_arg_2; SORT_1 var_49_arg_0 = var_48; SORT_3 var_49_arg_1 = state_45; SORT_3 var_49_arg_2 = var_44; SORT_3 var_49 = var_49_arg_0 ? var_49_arg_1 : var_49_arg_2; SORT_1 var_54_arg_0 = var_53; SORT_3 var_54_arg_1 = state_50; SORT_3 var_54_arg_2 = var_49; SORT_3 var_54 = var_54_arg_0 ? var_54_arg_1 : var_54_arg_2; SORT_1 var_58_arg_0 = var_57; SORT_3 var_58_arg_1 = state_55; SORT_3 var_58_arg_2 = var_54; SORT_3 var_58 = var_58_arg_0 ? var_58_arg_1 : var_58_arg_2; SORT_3 var_88_arg_0 = state_87; SORT_3 var_88_arg_1 = var_58; SORT_1 var_88 = var_88_arg_0 == var_88_arg_1; SORT_1 var_89_arg_0 = var_86; SORT_1 var_89_arg_1 = var_88; SORT_1 var_89 = var_89_arg_0 | var_89_arg_1; var_89 = var_89 & mask_SORT_1; SORT_1 var_110_arg_0 = state_91; SORT_1 var_110_arg_1 = input_109; SORT_1 var_110_arg_2 = var_89; SORT_1 var_110 = var_110_arg_0 ? var_110_arg_1 : var_110_arg_2; SORT_1 var_113_arg_0 = var_110; SORT_1 var_113 = ~var_113_arg_0; var_113 = var_113 & mask_SORT_1; SORT_1 var_114_arg_0 = var_112; SORT_1 var_114_arg_1 = var_113; SORT_1 var_114 = var_114_arg_0 & var_114_arg_1; var_114 = var_114 & mask_SORT_1; SORT_1 bad_115_arg_0 = var_114; __VERIFIER_assert(!(bad_115_arg_0)); // Computing next states ... SORT_11 var_137_arg_0 = state_136; SORT_13 var_137 = var_137_arg_0 >> 0; var_137 = var_137 & mask_SORT_13; SORT_13 var_194_arg_0 = var_137; SORT_13 var_194_arg_1 = var_15; SORT_1 var_194 = var_194_arg_0 == var_194_arg_1; SORT_1 var_195_arg_0 = input_6; SORT_1 var_195_arg_1 = var_194; SORT_1 var_195 = var_195_arg_0 & var_195_arg_1; var_195 = var_195 & mask_SORT_1; SORT_1 var_267_arg_0 = var_195; SORT_3 var_267_arg_1 = input_4; SORT_3 var_267_arg_2 = state_10; SORT_3 var_267 = var_267_arg_0 ? var_267_arg_1 : var_267_arg_2; SORT_1 var_269_arg_0 = input_7; SORT_3 var_269_arg_1 = var_268; SORT_3 var_269_arg_2 = var_267; SORT_3 var_269 = var_269_arg_0 ? var_269_arg_1 : var_269_arg_2; SORT_3 next_270_arg_1 = var_269; SORT_1 var_119_arg_0 = input_6; SORT_1 var_119_arg_1 = input_5; SORT_1 var_119 = var_119_arg_0 | var_119_arg_1; var_119 = var_119 & mask_SORT_1; SORT_1 var_120_arg_0 = var_119; SORT_1 var_120_arg_1 = input_7; SORT_1 var_120 = var_120_arg_0 | var_120_arg_1; var_120 = var_120 & mask_SORT_1; SORT_1 var_198_arg_0 = input_5; SORT_11 var_198 = var_198_arg_0; SORT_11 var_199_arg_0 = state_12; SORT_11 var_199_arg_1 = var_198; SORT_11 var_199 = var_199_arg_0 + var_199_arg_1; var_199 = var_199 & mask_SORT_11; SORT_1 var_271_arg_0 = var_120; SORT_11 var_271_arg_1 = var_199; SORT_11 var_271_arg_2 = state_12; SORT_11 var_271 = var_271_arg_0 ? var_271_arg_1 : var_271_arg_2; SORT_1 var_272_arg_0 = input_7; SORT_11 var_272_arg_1 = var_81; SORT_11 var_272_arg_2 = var_271; SORT_11 var_272 = var_272_arg_0 ? var_272_arg_1 : var_272_arg_2; SORT_11 next_273_arg_1 = var_272; SORT_19 var_187_arg_0 = var_20; SORT_13 var_187 = var_187_arg_0; SORT_13 var_188_arg_0 = var_137; SORT_13 var_188_arg_1 = var_187; SORT_1 var_188 = var_188_arg_0 == var_188_arg_1; 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_274_arg_0 = var_189; SORT_3 var_274_arg_1 = input_4; SORT_3 var_274_arg_2 = state_18; SORT_3 var_274 = var_274_arg_0 ? var_274_arg_1 : var_274_arg_2; SORT_1 var_275_arg_0 = input_7; SORT_3 var_275_arg_1 = var_268; SORT_3 var_275_arg_2 = var_274; SORT_3 var_275 = var_275_arg_0 ? var_275_arg_1 : var_275_arg_2; SORT_3 next_276_arg_1 = var_275; SORT_19 var_180_arg_0 = var_25; SORT_13 var_180 = var_180_arg_0; SORT_13 var_181_arg_0 = var_137; SORT_13 var_181_arg_1 = var_180; SORT_1 var_181 = var_181_arg_0 == var_181_arg_1; SORT_1 var_182_arg_0 = input_6; SORT_1 var_182_arg_1 = var_181; SORT_1 var_182 = var_182_arg_0 & var_182_arg_1; var_182 = var_182 & mask_SORT_1; SORT_1 var_277_arg_0 = var_182; SORT_3 var_277_arg_1 = input_4; SORT_3 var_277_arg_2 = state_24; SORT_3 var_277 = var_277_arg_0 ? var_277_arg_1 : var_277_arg_2; SORT_1 var_278_arg_0 = input_7; SORT_3 var_278_arg_1 = var_268; SORT_3 var_278_arg_2 = var_277; SORT_3 var_278 = var_278_arg_0 ? var_278_arg_1 : var_278_arg_2; SORT_3 next_279_arg_1 = var_278; SORT_19 var_173_arg_0 = var_30; SORT_13 var_173 = var_173_arg_0; SORT_13 var_174_arg_0 = var_137; SORT_13 var_174_arg_1 = var_173; SORT_1 var_174 = var_174_arg_0 == var_174_arg_1; SORT_1 var_175_arg_0 = input_6; SORT_1 var_175_arg_1 = var_174; SORT_1 var_175 = var_175_arg_0 & var_175_arg_1; var_175 = var_175 & mask_SORT_1; SORT_1 var_280_arg_0 = var_175; SORT_3 var_280_arg_1 = input_4; SORT_3 var_280_arg_2 = state_29; SORT_3 var_280 = var_280_arg_0 ? var_280_arg_1 : var_280_arg_2; SORT_1 var_281_arg_0 = input_7; SORT_3 var_281_arg_1 = var_268; SORT_3 var_281_arg_2 = var_280; SORT_3 var_281 = var_281_arg_0 ? var_281_arg_1 : var_281_arg_2; SORT_3 next_282_arg_1 = var_281; SORT_19 var_166_arg_0 = var_35; SORT_13 var_166 = var_166_arg_0; SORT_13 var_167_arg_0 = var_137; SORT_13 var_167_arg_1 = var_166; SORT_1 var_167 = var_167_arg_0 == var_167_arg_1; SORT_1 var_168_arg_0 = input_6; SORT_1 var_168_arg_1 = var_167; SORT_1 var_168 = var_168_arg_0 & var_168_arg_1; var_168 = var_168 & mask_SORT_1; SORT_1 var_283_arg_0 = var_168; SORT_3 var_283_arg_1 = input_4; SORT_3 var_283_arg_2 = state_34; SORT_3 var_283 = var_283_arg_0 ? var_283_arg_1 : var_283_arg_2; SORT_1 var_284_arg_0 = input_7; SORT_3 var_284_arg_1 = var_268; SORT_3 var_284_arg_2 = var_283; SORT_3 var_284 = var_284_arg_0 ? var_284_arg_1 : var_284_arg_2; SORT_3 next_285_arg_1 = var_284; SORT_40 var_159_arg_0 = var_41; SORT_13 var_159 = var_159_arg_0; SORT_13 var_160_arg_0 = var_137; SORT_13 var_160_arg_1 = var_159; SORT_1 var_160 = var_160_arg_0 == var_160_arg_1; SORT_1 var_161_arg_0 = input_6; SORT_1 var_161_arg_1 = var_160; SORT_1 var_161 = var_161_arg_0 & var_161_arg_1; var_161 = var_161 & mask_SORT_1; SORT_1 var_286_arg_0 = var_161; SORT_3 var_286_arg_1 = input_4; SORT_3 var_286_arg_2 = state_39; SORT_3 var_286 = var_286_arg_0 ? var_286_arg_1 : var_286_arg_2; SORT_1 var_287_arg_0 = input_7; SORT_3 var_287_arg_1 = var_268; SORT_3 var_287_arg_2 = var_286; SORT_3 var_287 = var_287_arg_0 ? var_287_arg_1 : var_287_arg_2; SORT_3 next_288_arg_1 = var_287; SORT_40 var_152_arg_0 = var_46; SORT_13 var_152 = var_152_arg_0; SORT_13 var_153_arg_0 = var_137; SORT_13 var_153_arg_1 = var_152; SORT_1 var_153 = var_153_arg_0 == var_153_arg_1; SORT_1 var_154_arg_0 = input_6; SORT_1 var_154_arg_1 = var_153; SORT_1 var_154 = var_154_arg_0 & var_154_arg_1; var_154 = var_154 & mask_SORT_1; SORT_1 var_289_arg_0 = var_154; SORT_3 var_289_arg_1 = input_4; SORT_3 var_289_arg_2 = state_45; SORT_3 var_289 = var_289_arg_0 ? var_289_arg_1 : var_289_arg_2; SORT_1 var_290_arg_0 = input_7; SORT_3 var_290_arg_1 = var_268; SORT_3 var_290_arg_2 = var_289; SORT_3 var_290 = var_290_arg_0 ? var_290_arg_1 : var_290_arg_2; SORT_3 next_291_arg_1 = var_290; SORT_1 var_145_arg_0 = var_51; SORT_13 var_145 = var_145_arg_0; SORT_13 var_146_arg_0 = var_137; SORT_13 var_146_arg_1 = var_145; SORT_1 var_146 = var_146_arg_0 == var_146_arg_1; SORT_1 var_147_arg_0 = input_6; SORT_1 var_147_arg_1 = var_146; SORT_1 var_147 = var_147_arg_0 & var_147_arg_1; var_147 = var_147 & mask_SORT_1; SORT_1 var_292_arg_0 = var_147; SORT_3 var_292_arg_1 = input_4; SORT_3 var_292_arg_2 = state_50; SORT_3 var_292 = var_292_arg_0 ? var_292_arg_1 : var_292_arg_2; SORT_1 var_293_arg_0 = input_7; SORT_3 var_293_arg_1 = var_268; SORT_3 var_293_arg_2 = var_292; SORT_3 var_293 = var_293_arg_0 ? var_293_arg_1 : var_293_arg_2; SORT_3 next_294_arg_1 = var_293; SORT_13 var_138_arg_0 = var_137; SORT_1 var_138 = var_138_arg_0 != 0; SORT_1 var_139_arg_0 = var_138; SORT_1 var_139 = ~var_139_arg_0; var_139 = var_139 & mask_SORT_1; SORT_1 var_140_arg_0 = input_6; SORT_1 var_140_arg_1 = var_139; SORT_1 var_140 = var_140_arg_0 & var_140_arg_1; var_140 = var_140 & mask_SORT_1; SORT_1 var_295_arg_0 = var_140; SORT_3 var_295_arg_1 = input_4; SORT_3 var_295_arg_2 = state_55; SORT_3 var_295 = var_295_arg_0 ? var_295_arg_1 : var_295_arg_2; SORT_1 var_296_arg_0 = input_7; SORT_3 var_296_arg_1 = var_268; SORT_3 var_296_arg_2 = var_295; SORT_3 var_296 = var_296_arg_0 ? var_296_arg_1 : var_296_arg_2; SORT_3 next_297_arg_1 = var_296; SORT_1 var_298_arg_0 = input_6; SORT_11 var_298 = var_298_arg_0; SORT_11 var_299_arg_0 = state_60; SORT_11 var_299_arg_1 = var_298; SORT_11 var_299 = var_299_arg_0 + var_299_arg_1; var_299 = var_299 & mask_SORT_11; SORT_1 var_300_arg_0 = input_5; SORT_11 var_300 = var_300_arg_0; SORT_11 var_301_arg_0 = var_299; SORT_11 var_301_arg_1 = var_300; SORT_11 var_301 = var_301_arg_0 - var_301_arg_1; var_301 = var_301 & mask_SORT_11; SORT_1 var_302_arg_0 = input_7; SORT_11 var_302_arg_1 = var_81; SORT_11 var_302_arg_2 = var_301; SORT_11 var_302 = var_302_arg_0 ? var_302_arg_1 : var_302_arg_2; SORT_11 next_303_arg_1 = var_302; SORT_1 var_228_arg_0 = state_68; SORT_1 var_228 = ~var_228_arg_0; var_228 = var_228 & mask_SORT_1; SORT_1 var_224_arg_0 = input_8; SORT_1 var_224_arg_1 = input_6; SORT_1 var_224 = var_224_arg_0 & var_224_arg_1; var_224 = var_224 & mask_SORT_1; SORT_1 var_225_arg_0 = state_68; SORT_1 var_225_arg_1 = var_224; SORT_1 var_225 = var_225_arg_0 | var_225_arg_1; var_225 = var_225 & mask_SORT_1; SORT_1 var_304_arg_0 = var_228; SORT_1 var_304_arg_1 = var_225; SORT_1 var_304_arg_2 = state_68; SORT_1 var_304 = var_304_arg_0 ? var_304_arg_1 : var_304_arg_2; SORT_1 var_305_arg_0 = input_7; SORT_1 var_305_arg_1 = var_111; SORT_1 var_305_arg_2 = var_304; SORT_1 var_305 = var_305_arg_0 ? var_305_arg_1 : var_305_arg_2; SORT_1 next_306_arg_1 = var_305; SORT_1 var_236_arg_0 = var_85; SORT_1 var_236_arg_1 = state_69; SORT_1 var_236 = var_236_arg_0 | var_236_arg_1; var_236 = var_236 & mask_SORT_1; SORT_1 var_307_arg_0 = var_51; SORT_1 var_307_arg_1 = var_236; SORT_1 var_307_arg_2 = state_69; SORT_1 var_307 = var_307_arg_0 ? var_307_arg_1 : var_307_arg_2; SORT_1 var_308_arg_0 = input_7; SORT_1 var_308_arg_1 = var_111; SORT_1 var_308_arg_2 = var_307; SORT_1 var_308 = var_308_arg_0 ? var_308_arg_1 : var_308_arg_2; SORT_1 next_309_arg_1 = var_308; SORT_1 var_248_arg_0 = input_6; SORT_1 var_248_arg_1 = input_5; SORT_1 var_248 = var_248_arg_0 | var_248_arg_1; var_248 = var_248 & mask_SORT_1; SORT_1 var_249_arg_0 = var_248; SORT_1 var_249_arg_1 = input_7; SORT_1 var_249 = var_249_arg_0 | var_249_arg_1; var_249 = var_249 & mask_SORT_1; SORT_1 var_250_arg_0 = var_249; SORT_1 var_250_arg_1 = state_68; SORT_1 var_250 = var_250_arg_0 | var_250_arg_1; var_250 = var_250 & mask_SORT_1; SORT_1 var_310_arg_0 = var_250; SORT_11 var_310_arg_1 = var_82; SORT_11 var_310_arg_2 = state_72; SORT_11 var_310 = var_310_arg_0 ? var_310_arg_1 : var_310_arg_2; SORT_1 var_311_arg_0 = input_7; SORT_11 var_311_arg_1 = var_81; SORT_11 var_311_arg_2 = var_310; SORT_11 var_311 = var_311_arg_0 ? var_311_arg_1 : var_311_arg_2; SORT_11 next_312_arg_1 = var_311; SORT_1 var_233_arg_0 = var_224; SORT_1 var_233_arg_1 = var_228; SORT_1 var_233 = var_233_arg_0 & var_233_arg_1; var_233 = var_233 & mask_SORT_1; SORT_1 var_313_arg_0 = var_233; SORT_3 var_313_arg_1 = input_4; SORT_3 var_313_arg_2 = state_87; SORT_3 var_313 = var_313_arg_0 ? var_313_arg_1 : var_313_arg_2; SORT_1 var_314_arg_0 = input_7; SORT_3 var_314_arg_1 = var_268; SORT_3 var_314_arg_2 = var_313; SORT_3 var_314 = var_314_arg_0 ? var_314_arg_1 : var_314_arg_2; SORT_3 next_315_arg_1 = var_314; SORT_1 next_316_arg_1 = var_111; SORT_1 var_204_arg_0 = input_6; SORT_11 var_204 = var_204_arg_0; SORT_11 var_205_arg_0 = state_136; SORT_11 var_205_arg_1 = var_204; SORT_11 var_205 = var_205_arg_0 + var_205_arg_1; var_205 = var_205 & mask_SORT_11; SORT_1 var_317_arg_0 = var_120; SORT_11 var_317_arg_1 = var_205; SORT_11 var_317_arg_2 = state_136; SORT_11 var_317 = var_317_arg_0 ? var_317_arg_1 : var_317_arg_2; SORT_1 var_318_arg_0 = input_7; SORT_11 var_318_arg_1 = var_81; SORT_11 var_318_arg_2 = var_317; SORT_11 var_318 = var_318_arg_0 ? var_318_arg_1 : var_318_arg_2; SORT_11 next_319_arg_1 = var_318; // Assigning next states ... state_10 = next_270_arg_1; state_12 = next_273_arg_1; state_18 = next_276_arg_1; state_24 = next_279_arg_1; state_29 = next_282_arg_1; state_34 = next_285_arg_1; state_39 = next_288_arg_1; state_45 = next_291_arg_1; state_50 = next_294_arg_1; state_55 = next_297_arg_1; state_60 = next_303_arg_1; state_68 = next_306_arg_1; state_69 = next_309_arg_1; state_72 = next_312_arg_1; state_87 = next_315_arg_1; state_91 = next_316_arg_1; state_136 = next_319_arg_1; } return 0; }