// 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+458 (git sha1 9b2b0d91, clang 6.0.0-1ubuntu2 -fPIC -Os) for module wrapper. 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", "safe_analog_estimation_convergence.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 int SORT_9; // BV with 31 bits const SORT_9 mask_SORT_9 = (SORT_9)-1 >> (sizeof(SORT_9) * 8 - 31); const SORT_9 msb_SORT_9 = (SORT_9)1 << (31 - 1); typedef unsigned short SORT_11; // BV with 16 bits const SORT_11 mask_SORT_11 = (SORT_11)-1 >> (sizeof(SORT_11) * 8 - 16); const SORT_11 msb_SORT_11 = (SORT_11)1 << (16 - 1); typedef unsigned char SORT_12; // BV with 8 bits const SORT_12 mask_SORT_12 = (SORT_12)-1 >> (sizeof(SORT_12) * 8 - 8); const SORT_12 msb_SORT_12 = (SORT_12)1 << (8 - 1); typedef unsigned int SORT_20; // BV with 32 bits const SORT_20 mask_SORT_20 = (SORT_20)-1 >> (sizeof(SORT_20) * 8 - 32); const SORT_20 msb_SORT_20 = (SORT_20)1 << (32 - 1); typedef unsigned int SORT_23; // BV with 17 bits const SORT_23 mask_SORT_23 = (SORT_23)-1 >> (sizeof(SORT_23) * 8 - 17); const SORT_23 msb_SORT_23 = (SORT_23)1 << (17 - 1); typedef unsigned int SORT_26; // BV with 18 bits const SORT_26 mask_SORT_26 = (SORT_26)-1 >> (sizeof(SORT_26) * 8 - 18); const SORT_26 msb_SORT_26 = (SORT_26)1 << (18 - 1); typedef unsigned int SORT_29; // BV with 19 bits const SORT_29 mask_SORT_29 = (SORT_29)-1 >> (sizeof(SORT_29) * 8 - 19); const SORT_29 msb_SORT_29 = (SORT_29)1 << (19 - 1); typedef unsigned int SORT_32; // BV with 20 bits const SORT_32 mask_SORT_32 = (SORT_32)-1 >> (sizeof(SORT_32) * 8 - 20); const SORT_32 msb_SORT_32 = (SORT_32)1 << (20 - 1); typedef unsigned int SORT_35; // BV with 21 bits const SORT_35 mask_SORT_35 = (SORT_35)-1 >> (sizeof(SORT_35) * 8 - 21); const SORT_35 msb_SORT_35 = (SORT_35)1 << (21 - 1); typedef unsigned int SORT_38; // BV with 22 bits const SORT_38 mask_SORT_38 = (SORT_38)-1 >> (sizeof(SORT_38) * 8 - 22); const SORT_38 msb_SORT_38 = (SORT_38)1 << (22 - 1); typedef unsigned int SORT_41; // BV with 23 bits const SORT_41 mask_SORT_41 = (SORT_41)-1 >> (sizeof(SORT_41) * 8 - 23); const SORT_41 msb_SORT_41 = (SORT_41)1 << (23 - 1); typedef unsigned int SORT_44; // BV with 24 bits const SORT_44 mask_SORT_44 = (SORT_44)-1 >> (sizeof(SORT_44) * 8 - 24); const SORT_44 msb_SORT_44 = (SORT_44)1 << (24 - 1); typedef unsigned int SORT_47; // BV with 25 bits const SORT_47 mask_SORT_47 = (SORT_47)-1 >> (sizeof(SORT_47) * 8 - 25); const SORT_47 msb_SORT_47 = (SORT_47)1 << (25 - 1); typedef unsigned int SORT_50; // BV with 26 bits const SORT_50 mask_SORT_50 = (SORT_50)-1 >> (sizeof(SORT_50) * 8 - 26); const SORT_50 msb_SORT_50 = (SORT_50)1 << (26 - 1); typedef unsigned int SORT_53; // BV with 27 bits const SORT_53 mask_SORT_53 = (SORT_53)-1 >> (sizeof(SORT_53) * 8 - 27); const SORT_53 msb_SORT_53 = (SORT_53)1 << (27 - 1); typedef unsigned int SORT_56; // BV with 28 bits const SORT_56 mask_SORT_56 = (SORT_56)-1 >> (sizeof(SORT_56) * 8 - 28); const SORT_56 msb_SORT_56 = (SORT_56)1 << (28 - 1); typedef unsigned int SORT_59; // BV with 29 bits const SORT_59 mask_SORT_59 = (SORT_59)-1 >> (sizeof(SORT_59) * 8 - 29); const SORT_59 msb_SORT_59 = (SORT_59)1 << (29 - 1); typedef unsigned int SORT_62; // BV with 30 bits const SORT_62 mask_SORT_62 = (SORT_62)-1 >> (sizeof(SORT_62) * 8 - 30); const SORT_62 msb_SORT_62 = (SORT_62)1 << (30 - 1); typedef unsigned char SORT_72; // BV with 3 bits const SORT_72 mask_SORT_72 = (SORT_72)-1 >> (sizeof(SORT_72) * 8 - 3); const SORT_72 msb_SORT_72 = (SORT_72)1 << (3 - 1); typedef unsigned char SORT_96; // BV with 4 bits const SORT_96 mask_SORT_96 = (SORT_96)-1 >> (sizeof(SORT_96) * 8 - 4); const SORT_96 msb_SORT_96 = (SORT_96)1 << (4 - 1); typedef unsigned short SORT_101; // BV with 14 bits const SORT_101 mask_SORT_101 = (SORT_101)-1 >> (sizeof(SORT_101) * 8 - 14); const SORT_101 msb_SORT_101 = (SORT_101)1 << (14 - 1); typedef unsigned char SORT_105; // BV with 2 bits const SORT_105 mask_SORT_105 = (SORT_105)-1 >> (sizeof(SORT_105) * 8 - 2); const SORT_105 msb_SORT_105 = (SORT_105)1 << (2 - 1); typedef unsigned char SORT_154; // BV with 7 bits const SORT_154 mask_SORT_154 = (SORT_154)-1 >> (sizeof(SORT_154) * 8 - 7); const SORT_154 msb_SORT_154 = (SORT_154)1 << (7 - 1); // Initializing constants ... const SORT_1 var_7 = 0; const SORT_1 var_8 = 1; const SORT_9 var_10 = 0; const SORT_12 var_13 = 0; const SORT_12 var_14 = 200; const SORT_72 var_73 = 5; const SORT_11 var_75 = 0; const SORT_105 var_106 = 1; const SORT_12 var_112 = 127; const SORT_11 var_119 = 64; const SORT_11 var_121 = 1; const SORT_11 var_123 = 127; const SORT_11 var_126 = 200; const SORT_72 var_131 = 4; const SORT_72 var_134 = 6; const SORT_96 var_138 = 9; const SORT_154 var_155 = 64; const SORT_72 var_166 = 0; const SORT_96 var_169 = 0; // Collecting input declarations ... SORT_1 input_2; SORT_1 input_3; SORT_1 input_4; // Collecting state declarations ... SORT_1 state_5 = __VERIFIER_nondet_uchar() & mask_SORT_1; SORT_11 state_17 = __VERIFIER_nondet_ushort() & mask_SORT_11; SORT_11 state_76 = __VERIFIER_nondet_ushort() & mask_SORT_11; SORT_96 state_97 = __VERIFIER_nondet_uchar() & mask_SORT_96; SORT_96 state_100 = __VERIFIER_nondet_uchar() & mask_SORT_96; // Initializing states ... SORT_11 init_77_arg_1 = var_75; state_76 = init_77_arg_1; for (;;) { // Getting external input values ... input_2 = __VERIFIER_nondet_uchar(); input_3 = __VERIFIER_nondet_uchar(); input_3 = input_3 & mask_SORT_1; input_4 = __VERIFIER_nondet_uchar(); input_4 = input_4 & mask_SORT_1; // Assuming invariants ... SORT_1 var_84_arg_0 = state_5; SORT_1 var_84 = ~var_84_arg_0; SORT_1 var_85_arg_0 = var_84; SORT_1 var_85 = ~var_85_arg_0; SORT_1 var_86_arg_0 = state_5; SORT_1 var_86_arg_1 = var_85; SORT_1 var_86 = var_86_arg_0 | var_86_arg_1; var_86 = var_86 & mask_SORT_1; SORT_1 constr_87_arg_0 = var_86; assume_abort_if_not(constr_87_arg_0); SORT_1 var_88_arg_0 = var_8; var_88_arg_0 = var_88_arg_0 & mask_SORT_1; SORT_11 var_88 = var_88_arg_0; SORT_11 var_89_arg_0 = state_76; SORT_11 var_89_arg_1 = var_88; SORT_1 var_89 = var_89_arg_0 <= var_89_arg_1; SORT_1 var_90_arg_0 = input_4; SORT_1 var_90_arg_1 = var_89; SORT_1 var_90 = var_90_arg_0 ^ var_90_arg_1; SORT_1 var_91_arg_0 = var_90; SORT_1 var_91 = ~var_91_arg_0; SORT_1 var_92_arg_0 = var_90; SORT_1 var_92 = ~var_92_arg_0; SORT_1 var_93_arg_0 = var_91; SORT_1 var_93_arg_1 = var_92; SORT_1 var_93 = var_93_arg_0 | var_93_arg_1; var_93 = var_93 & mask_SORT_1; SORT_1 constr_94_arg_0 = var_93; assume_abort_if_not(constr_94_arg_0); // Asserting properties ... SORT_72 var_74_arg_0 = var_73; var_74_arg_0 = var_74_arg_0 & mask_SORT_72; SORT_11 var_74 = var_74_arg_0; SORT_11 var_78_arg_0 = var_74; SORT_11 var_78_arg_1 = state_76; SORT_1 var_78 = var_78_arg_0 < var_78_arg_1; SORT_1 var_15_arg_0 = input_3; SORT_12 var_15_arg_1 = var_14; SORT_12 var_15_arg_2 = var_13; SORT_12 var_15 = var_15_arg_0 ? var_15_arg_1 : var_15_arg_2; var_15 = var_15 & mask_SORT_12; SORT_12 var_16_arg_0 = var_13; SORT_12 var_16_arg_1 = var_15; SORT_11 var_16 = ((SORT_11)var_16_arg_0 << 8) | var_16_arg_1; SORT_11 var_18_arg_0 = var_16; SORT_11 var_18_arg_1 = state_17; SORT_11 var_18 = var_18_arg_0 - var_18_arg_1; var_18 = var_18 & mask_SORT_11; SORT_11 var_19_arg_0 = var_18; SORT_1 var_19 = var_19_arg_0 >> 15; SORT_1 var_21_arg_0 = var_19; SORT_9 var_21_arg_1 = var_10; SORT_20 var_21 = ((SORT_20)var_21_arg_0 << 31) | var_21_arg_1; var_21 = var_21 & mask_SORT_20; SORT_11 var_64_arg_0 = var_18; SORT_1 var_64 = var_64_arg_0 >> 15; SORT_11 var_61_arg_0 = var_18; SORT_1 var_61 = var_61_arg_0 >> 15; SORT_11 var_58_arg_0 = var_18; SORT_1 var_58 = var_58_arg_0 >> 15; SORT_11 var_55_arg_0 = var_18; SORT_1 var_55 = var_55_arg_0 >> 15; SORT_11 var_52_arg_0 = var_18; SORT_1 var_52 = var_52_arg_0 >> 15; SORT_11 var_49_arg_0 = var_18; SORT_1 var_49 = var_49_arg_0 >> 15; SORT_11 var_46_arg_0 = var_18; SORT_1 var_46 = var_46_arg_0 >> 15; SORT_11 var_43_arg_0 = var_18; SORT_1 var_43 = var_43_arg_0 >> 15; SORT_11 var_40_arg_0 = var_18; SORT_1 var_40 = var_40_arg_0 >> 15; SORT_11 var_37_arg_0 = var_18; SORT_1 var_37 = var_37_arg_0 >> 15; SORT_11 var_34_arg_0 = var_18; SORT_1 var_34 = var_34_arg_0 >> 15; SORT_11 var_31_arg_0 = var_18; SORT_1 var_31 = var_31_arg_0 >> 15; SORT_11 var_28_arg_0 = var_18; SORT_1 var_28 = var_28_arg_0 >> 15; SORT_11 var_25_arg_0 = var_18; SORT_1 var_25 = var_25_arg_0 >> 15; SORT_11 var_22_arg_0 = var_18; SORT_1 var_22 = var_22_arg_0 >> 15; SORT_1 var_24_arg_0 = var_22; SORT_11 var_24_arg_1 = var_18; SORT_23 var_24 = ((SORT_23)var_24_arg_0 << 16) | var_24_arg_1; var_24 = var_24 & mask_SORT_23; SORT_1 var_27_arg_0 = var_25; SORT_23 var_27_arg_1 = var_24; SORT_26 var_27 = ((SORT_26)var_27_arg_0 << 17) | var_27_arg_1; var_27 = var_27 & mask_SORT_26; SORT_1 var_30_arg_0 = var_28; SORT_26 var_30_arg_1 = var_27; SORT_29 var_30 = ((SORT_29)var_30_arg_0 << 18) | var_30_arg_1; var_30 = var_30 & mask_SORT_29; SORT_1 var_33_arg_0 = var_31; SORT_29 var_33_arg_1 = var_30; SORT_32 var_33 = ((SORT_32)var_33_arg_0 << 19) | var_33_arg_1; var_33 = var_33 & mask_SORT_32; SORT_1 var_36_arg_0 = var_34; SORT_32 var_36_arg_1 = var_33; SORT_35 var_36 = ((SORT_35)var_36_arg_0 << 20) | var_36_arg_1; var_36 = var_36 & mask_SORT_35; SORT_1 var_39_arg_0 = var_37; SORT_35 var_39_arg_1 = var_36; SORT_38 var_39 = ((SORT_38)var_39_arg_0 << 21) | var_39_arg_1; var_39 = var_39 & mask_SORT_38; SORT_1 var_42_arg_0 = var_40; SORT_38 var_42_arg_1 = var_39; SORT_41 var_42 = ((SORT_41)var_42_arg_0 << 22) | var_42_arg_1; var_42 = var_42 & mask_SORT_41; SORT_1 var_45_arg_0 = var_43; SORT_41 var_45_arg_1 = var_42; SORT_44 var_45 = ((SORT_44)var_45_arg_0 << 23) | var_45_arg_1; var_45 = var_45 & mask_SORT_44; SORT_1 var_48_arg_0 = var_46; SORT_44 var_48_arg_1 = var_45; SORT_47 var_48 = ((SORT_47)var_48_arg_0 << 24) | var_48_arg_1; var_48 = var_48 & mask_SORT_47; SORT_1 var_51_arg_0 = var_49; SORT_47 var_51_arg_1 = var_48; SORT_50 var_51 = ((SORT_50)var_51_arg_0 << 25) | var_51_arg_1; var_51 = var_51 & mask_SORT_50; SORT_1 var_54_arg_0 = var_52; SORT_50 var_54_arg_1 = var_51; SORT_53 var_54 = ((SORT_53)var_54_arg_0 << 26) | var_54_arg_1; var_54 = var_54 & mask_SORT_53; SORT_1 var_57_arg_0 = var_55; SORT_53 var_57_arg_1 = var_54; SORT_56 var_57 = ((SORT_56)var_57_arg_0 << 27) | var_57_arg_1; var_57 = var_57 & mask_SORT_56; SORT_1 var_60_arg_0 = var_58; SORT_56 var_60_arg_1 = var_57; SORT_59 var_60 = ((SORT_59)var_60_arg_0 << 28) | var_60_arg_1; var_60 = var_60 & mask_SORT_59; SORT_1 var_63_arg_0 = var_61; SORT_59 var_63_arg_1 = var_60; SORT_62 var_63 = ((SORT_62)var_63_arg_0 << 29) | var_63_arg_1; var_63 = var_63 & mask_SORT_62; SORT_1 var_65_arg_0 = var_64; SORT_62 var_65_arg_1 = var_63; SORT_9 var_65 = ((SORT_9)var_65_arg_0 << 30) | var_65_arg_1; SORT_9 var_66_arg_0 = var_65; var_66_arg_0 = var_66_arg_0 & mask_SORT_9; SORT_20 var_66 = var_66_arg_0; SORT_20 var_67_arg_0 = var_21; SORT_20 var_67_arg_1 = var_66; SORT_1 var_67 = var_67_arg_0 <= var_67_arg_1; SORT_1 var_68_arg_0 = var_67; SORT_1 var_68_arg_1 = var_8; SORT_1 var_68_arg_2 = var_7; SORT_1 var_68 = var_68_arg_0 ? var_68_arg_1 : var_68_arg_2; SORT_1 var_69_arg_0 = input_3; SORT_1 var_69_arg_1 = var_68; SORT_1 var_69 = var_69_arg_0 ^ var_69_arg_1; SORT_1 var_70_arg_0 = var_69; SORT_1 var_70 = ~var_70_arg_0; SORT_1 var_79_arg_0 = var_78; SORT_1 var_79_arg_1 = var_70; SORT_1 var_79_arg_2 = var_8; SORT_1 var_79 = var_79_arg_0 ? var_79_arg_1 : var_79_arg_2; SORT_1 var_80_arg_0 = var_79; SORT_1 var_80 = ~var_80_arg_0; SORT_1 var_81_arg_0 = var_79; SORT_1 var_81 = ~var_81_arg_0; SORT_1 var_82_arg_0 = var_80; SORT_1 var_82_arg_1 = var_81; SORT_1 var_82 = var_82_arg_0 & var_82_arg_1; var_82 = var_82 & mask_SORT_1; SORT_1 bad_83_arg_0 = var_82; __VERIFIER_assert(!(bad_83_arg_0)); // Computing next states ... SORT_96 var_139_arg_0 = state_100; SORT_96 var_139_arg_1 = var_138; SORT_1 var_139 = var_139_arg_0 == var_139_arg_1; SORT_72 var_132_arg_0 = var_131; var_132_arg_0 = var_132_arg_0 & mask_SORT_72; SORT_96 var_132 = var_132_arg_0; SORT_96 var_133_arg_0 = var_132; SORT_96 var_133_arg_1 = state_97; SORT_1 var_133 = var_133_arg_0 <= var_133_arg_1; SORT_72 var_135_arg_0 = var_134; var_135_arg_0 = var_135_arg_0 & mask_SORT_72; SORT_96 var_135 = var_135_arg_0; SORT_96 var_136_arg_0 = state_97; SORT_96 var_136_arg_1 = var_135; SORT_1 var_136 = var_136_arg_0 <= var_136_arg_1; SORT_1 var_137_arg_0 = var_133; SORT_1 var_137_arg_1 = var_136; SORT_1 var_137 = var_137_arg_0 & var_137_arg_1; SORT_1 var_140_arg_0 = var_139; SORT_1 var_140_arg_1 = var_137; SORT_1 var_140_arg_2 = var_8; SORT_1 var_140 = var_140_arg_0 ? var_140_arg_1 : var_140_arg_2; SORT_1 var_141_arg_0 = input_4; SORT_1 var_141_arg_1 = var_8; SORT_1 var_141_arg_2 = var_140; SORT_1 var_141 = var_141_arg_0 ? var_141_arg_1 : var_141_arg_2; SORT_1 next_142_arg_1 = var_141; SORT_12 var_113_arg_0 = var_112; var_113_arg_0 = (var_113_arg_0 & msb_SORT_12) ? (var_113_arg_0 | ~mask_SORT_12) : (var_113_arg_0 & mask_SORT_12); SORT_41 var_113 = (int)((signed char)var_113_arg_0); SORT_11 var_114_arg_0 = state_17; var_114_arg_0 = (var_114_arg_0 & msb_SORT_11) ? (var_114_arg_0 | ~mask_SORT_11) : (var_114_arg_0 & mask_SORT_11); SORT_41 var_114 = (int)((short)var_114_arg_0); SORT_41 var_115_arg_0 = var_113; SORT_41 var_115_arg_1 = var_114; SORT_41 var_115 = var_115_arg_0 * var_115_arg_1; SORT_105 var_107_arg_0 = var_106; var_107_arg_0 = (var_107_arg_0 & msb_SORT_105) ? (var_107_arg_0 | ~mask_SORT_105) : (var_107_arg_0 & mask_SORT_105); SORT_26 var_107 = (int)((signed char)var_107_arg_0); SORT_11 var_108_arg_0 = var_16; var_108_arg_0 = (var_108_arg_0 & msb_SORT_11) ? (var_108_arg_0 | ~mask_SORT_11) : (var_108_arg_0 & mask_SORT_11); SORT_26 var_108 = (int)((short)var_108_arg_0); SORT_26 var_109_arg_0 = var_107; SORT_26 var_109_arg_1 = var_108; SORT_26 var_109 = var_109_arg_0 * var_109_arg_1; var_109 = var_109 & mask_SORT_26; SORT_26 var_151_arg_0 = var_109; SORT_1 var_151 = var_151_arg_0 >> 17; SORT_26 var_149_arg_0 = var_109; SORT_1 var_149 = var_149_arg_0 >> 17; SORT_26 var_147_arg_0 = var_109; SORT_1 var_147 = var_147_arg_0 >> 17; SORT_26 var_145_arg_0 = var_109; SORT_1 var_145 = var_145_arg_0 >> 17; SORT_26 var_143_arg_0 = var_109; SORT_1 var_143 = var_143_arg_0 >> 17; SORT_1 var_144_arg_0 = var_143; SORT_26 var_144_arg_1 = var_109; SORT_29 var_144 = ((SORT_29)var_144_arg_0 << 18) | var_144_arg_1; var_144 = var_144 & mask_SORT_29; SORT_1 var_146_arg_0 = var_145; SORT_29 var_146_arg_1 = var_144; SORT_32 var_146 = ((SORT_32)var_146_arg_0 << 19) | var_146_arg_1; var_146 = var_146 & mask_SORT_32; SORT_1 var_148_arg_0 = var_147; SORT_32 var_148_arg_1 = var_146; SORT_35 var_148 = ((SORT_35)var_148_arg_0 << 20) | var_148_arg_1; var_148 = var_148 & mask_SORT_35; SORT_1 var_150_arg_0 = var_149; SORT_35 var_150_arg_1 = var_148; SORT_38 var_150 = ((SORT_38)var_150_arg_0 << 21) | var_150_arg_1; var_150 = var_150 & mask_SORT_38; SORT_1 var_152_arg_0 = var_151; SORT_38 var_152_arg_1 = var_150; SORT_41 var_152 = ((SORT_41)var_152_arg_0 << 22) | var_152_arg_1; SORT_41 var_153_arg_0 = var_115; SORT_41 var_153_arg_1 = var_152; SORT_41 var_153 = var_153_arg_0 + var_153_arg_1; SORT_154 var_156_arg_0 = var_155; var_156_arg_0 = var_156_arg_0 & mask_SORT_154; SORT_41 var_156 = var_156_arg_0; SORT_41 var_157_arg_0 = var_153; SORT_41 var_157_arg_1 = var_156; SORT_41 var_157 = var_157_arg_0 + var_157_arg_1; SORT_41 var_158_arg_0 = var_157; SORT_11 var_158 = var_158_arg_0 >> 7; SORT_1 var_159_arg_0 = input_4; SORT_11 var_159_arg_1 = var_119; SORT_11 var_159_arg_2 = var_158; SORT_11 var_159 = var_159_arg_0 ? var_159_arg_1 : var_159_arg_2; SORT_11 next_160_arg_1 = var_159; SORT_1 var_161_arg_0 = var_8; var_161_arg_0 = var_161_arg_0 & mask_SORT_1; SORT_11 var_161 = var_161_arg_0; SORT_11 var_162_arg_0 = state_76; SORT_11 var_162_arg_1 = var_161; SORT_11 var_162 = var_162_arg_0 + var_162_arg_1; var_162 = var_162 & mask_SORT_11; SORT_11 next_163_arg_1 = var_162; SORT_72 var_167_arg_0 = var_166; SORT_1 var_167_arg_1 = input_3; SORT_96 var_167 = ((SORT_96)var_167_arg_0 << 1) | var_167_arg_1; SORT_1 var_164_arg_0 = input_3; var_164_arg_0 = var_164_arg_0 & mask_SORT_1; SORT_96 var_164 = var_164_arg_0; SORT_96 var_165_arg_0 = state_97; SORT_96 var_165_arg_1 = var_164; SORT_96 var_165 = var_165_arg_0 + var_165_arg_1; SORT_1 var_168_arg_0 = var_139; SORT_96 var_168_arg_1 = var_167; SORT_96 var_168_arg_2 = var_165; SORT_96 var_168 = var_168_arg_0 ? var_168_arg_1 : var_168_arg_2; SORT_1 var_170_arg_0 = input_4; SORT_96 var_170_arg_1 = var_169; SORT_96 var_170_arg_2 = var_168; SORT_96 var_170 = var_170_arg_0 ? var_170_arg_1 : var_170_arg_2; var_170 = var_170 & mask_SORT_96; SORT_96 next_171_arg_1 = var_170; SORT_1 var_172_arg_0 = var_8; var_172_arg_0 = var_172_arg_0 & mask_SORT_1; SORT_96 var_172 = var_172_arg_0; SORT_96 var_173_arg_0 = state_100; SORT_96 var_173_arg_1 = var_172; SORT_96 var_173 = var_173_arg_0 + var_173_arg_1; SORT_1 var_174_arg_0 = var_139; SORT_96 var_174_arg_1 = var_169; SORT_96 var_174_arg_2 = var_173; SORT_96 var_174 = var_174_arg_0 ? var_174_arg_1 : var_174_arg_2; SORT_1 var_175_arg_0 = input_4; SORT_96 var_175_arg_1 = var_169; SORT_96 var_175_arg_2 = var_174; SORT_96 var_175 = var_175_arg_0 ? var_175_arg_1 : var_175_arg_2; var_175 = var_175 & mask_SORT_96; SORT_96 next_176_arg_1 = var_175; // Assigning next states ... state_5 = next_142_arg_1; state_17 = next_160_arg_1; state_76 = next_163_arg_1; state_97 = next_171_arg_1; state_100 = next_176_arg_1; } return 0; }