// This file is part of the SV-Benchmarks collection of verification tasks:
// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
//
// SPDX-FileCopyrightText: 2020 Aman Goel
// SPDX-FileCopyrightText: 2022 The SV-Benchmarks Community
//
// SPDX-License-Identifier: GPL-3.0-or-later

// 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/aman-goel/avr/tree/92362931700b66684418a991d018c9fbdbebc06f/tests
// ; BTOR description generated by Yosys 0.9+431 (git sha1 4a3b5437, clang 4.0.1-6 -fPIC -Os) for module main.
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", "cal13.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_5;  // BV with 2 bits
  const SORT_5 mask_SORT_5 = (SORT_5)-1 >> (sizeof(SORT_5) * 8 - 2);
  const SORT_5 msb_SORT_5 = (SORT_5)1 << (2 - 1);
  // Initializing constants ...
  const SORT_1 var_10 = 0;
  const SORT_5 var_14 = 0;
  const SORT_1 var_29 = 1;
  const SORT_5 var_39 = 1;
  // Collecting input declarations ...
  SORT_1 input_2;
  SORT_1 input_3;
  SORT_1 input_4;
  SORT_5 input_6;
  SORT_1 input_7;
  SORT_5 input_8;
  SORT_5 input_9;
  // Collecting state declarations ...
  SORT_1 state_11 = __VERIFIER_nondet_uchar() & mask_SORT_1;
  SORT_5 state_15 = __VERIFIER_nondet_uchar() & mask_SORT_5;
  SORT_1 state_17 = __VERIFIER_nondet_uchar() & mask_SORT_1;
  SORT_5 state_21 = __VERIFIER_nondet_uchar() & mask_SORT_5;
  // Initializing states ...
  SORT_1 init_12_arg_1 = var_10;
  state_11 = init_12_arg_1;
  SORT_5 init_16_arg_1 = var_14;
  state_15 = init_16_arg_1;
  SORT_1 init_18_arg_1 = var_10;
  state_17 = init_18_arg_1;
  SORT_5 init_22_arg_1 = var_14;
  state_21 = init_22_arg_1;
  for (;;) {
    // Getting external input values ...
    input_2 = __VERIFIER_nondet_uchar();
    input_2 = input_2 & mask_SORT_1;
    input_3 = __VERIFIER_nondet_uchar();
    input_3 = input_3 & mask_SORT_1;
    input_4 = __VERIFIER_nondet_uchar();
    input_6 = __VERIFIER_nondet_uchar();
    input_7 = __VERIFIER_nondet_uchar();
    input_8 = __VERIFIER_nondet_uchar();
    input_9 = __VERIFIER_nondet_uchar();
    // Assuming invariants ...
    // Asserting properties ...
    SORT_1 var_13_arg_0 = state_11;
    SORT_1 var_13 = ~var_13_arg_0;
    SORT_1 var_19_arg_0 = state_17;
    SORT_5 var_19_arg_1 = state_15;
    SORT_5 var_19_arg_2 = input_6;
    SORT_5 var_19 = var_19_arg_0 ? var_19_arg_1 : var_19_arg_2;
    SORT_5 var_20_arg_0 = var_19;
    SORT_1 var_20 = var_20_arg_0 >> 1;
    var_20 = var_20 & mask_SORT_1;
    SORT_1 var_23_arg_0 = state_17;
    SORT_5 var_23_arg_1 = state_21;
    SORT_5 var_23_arg_2 = input_6;
    SORT_5 var_23 = var_23_arg_0 ? var_23_arg_1 : var_23_arg_2;
    SORT_5 var_24_arg_0 = var_23;
    SORT_1 var_24 = var_24_arg_0 >> 1;
    var_24 = var_24 & mask_SORT_1;
    SORT_1 var_25_arg_0 = var_20;
    SORT_1 var_25_arg_1 = var_24;
    SORT_1 var_25 = var_25_arg_0 == var_25_arg_1;
    SORT_1 var_26_arg_0 = var_13;
    SORT_1 var_26_arg_1 = var_25;
    SORT_1 var_26 = var_26_arg_0 | var_26_arg_1;
    SORT_1 var_30_arg_0 = var_26;
    SORT_1 var_30 = ~var_30_arg_0;
    SORT_1 var_31_arg_0 = var_29;
    SORT_1 var_31_arg_1 = var_30;
    SORT_1 var_31 = var_31_arg_0 & var_31_arg_1;
    var_31 = var_31 & mask_SORT_1;
    SORT_1 bad_32_arg_0 = var_31;
    __VERIFIER_assert(!(bad_32_arg_0));
    // Computing next states ...
    SORT_1 next_51_arg_1 = var_29;
    SORT_1 var_46_arg_0 = state_11;
    SORT_1 var_46 = ~var_46_arg_0;
    var_46 = var_46 & mask_SORT_1;
    SORT_1 var_36_arg_0 = input_4;
    SORT_1 var_36 = ~var_36_arg_0;
    var_36 = var_36 & mask_SORT_1;
    SORT_5 var_33_arg_0 = var_19;
    SORT_1 var_33 = var_33_arg_0 >> 0;
    var_33 = var_33 & mask_SORT_1;
    SORT_1 var_34_arg_0 = var_33;
    SORT_1 var_34_arg_1 = var_29;
    SORT_1 var_34_arg_2 = var_20;
    SORT_1 var_34 = var_34_arg_0 ? var_34_arg_1 : var_34_arg_2;
    SORT_1 var_35_arg_0 = var_34;
    SORT_1 var_35_arg_1 = var_10;
    SORT_5 var_35 = ((SORT_5)var_35_arg_0 << 1) | var_35_arg_1;
    SORT_1 var_37_arg_0 = var_36;
    SORT_5 var_37_arg_1 = var_35;
    SORT_5 var_37_arg_2 = var_19;
    SORT_5 var_37 = var_37_arg_0 ? var_37_arg_1 : var_37_arg_2;
    SORT_1 var_40_arg_0 = input_3;
    SORT_5 var_40_arg_1 = var_39;
    SORT_5 var_40_arg_2 = var_37;
    SORT_5 var_40 = var_40_arg_0 ? var_40_arg_1 : var_40_arg_2;
    SORT_1 var_44_arg_0 = input_2;
    SORT_5 var_44_arg_1 = var_40;
    SORT_5 var_44_arg_2 = var_19;
    SORT_5 var_44 = var_44_arg_0 ? var_44_arg_1 : var_44_arg_2;
    SORT_1 var_52_arg_0 = var_10;
    SORT_5 var_52_arg_1 = var_14;
    SORT_5 var_52_arg_2 = var_44;
    SORT_5 var_52 = var_52_arg_0 ? var_52_arg_1 : var_52_arg_2;
    SORT_1 var_53_arg_0 = var_46;
    SORT_5 var_53_arg_1 = input_9;
    SORT_5 var_53_arg_2 = var_52;
    SORT_5 var_53 = var_53_arg_0 ? var_53_arg_1 : var_53_arg_2;
    SORT_5 next_54_arg_1 = var_53;
    SORT_1 var_55_arg_0 = var_10;
    SORT_1 var_55_arg_1 = var_10;
    SORT_1 var_55_arg_2 = var_29;
    SORT_1 var_55 = var_55_arg_0 ? var_55_arg_1 : var_55_arg_2;
    SORT_1 var_56_arg_0 = var_46;
    SORT_1 var_56_arg_1 = var_10;
    SORT_1 var_56_arg_2 = var_55;
    SORT_1 var_56 = var_56_arg_0 ? var_56_arg_1 : var_56_arg_2;
    var_56 = var_56 & mask_SORT_1;
    SORT_1 next_57_arg_1 = var_56;
    SORT_1 var_58_arg_0 = var_10;
    SORT_5 var_58_arg_1 = var_14;
    SORT_5 var_58_arg_2 = var_44;
    SORT_5 var_58 = var_58_arg_0 ? var_58_arg_1 : var_58_arg_2;
    SORT_1 var_59_arg_0 = var_46;
    SORT_5 var_59_arg_1 = input_8;
    SORT_5 var_59_arg_2 = var_58;
    SORT_5 var_59 = var_59_arg_0 ? var_59_arg_1 : var_59_arg_2;
    SORT_5 next_60_arg_1 = var_59;
    // Assigning next states ...
    state_11 = next_51_arg_1;
    state_15 = next_54_arg_1;
    state_17 = next_57_arg_1;
    state_21 = next_60_arg_1;
  }
  return 0;
}