// 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=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/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", "vcegar_QF_BV_itc99_b13_p02.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_7;  // BV with 4 bits
  const SORT_7 mask_SORT_7 = (SORT_7)-1 >> (sizeof(SORT_7) * 8 - 4);
  const SORT_7 msb_SORT_7 = (SORT_7)1 << (4 - 1);
  typedef unsigned int SORT_12;  // BV with 32 bits
  const SORT_12 mask_SORT_12 = (SORT_12)-1 >> (sizeof(SORT_12) * 8 - 32);
  const SORT_12 msb_SORT_12 = (SORT_12)1 << (32 - 1);
  typedef unsigned short SORT_66;  // BV with 10 bits
  const SORT_66 mask_SORT_66 = (SORT_66)-1 >> (sizeof(SORT_66) * 8 - 10);
  const SORT_66 msb_SORT_66 = (SORT_66)1 << (10 - 1);
  // Initializing constants ...
  const SORT_7 var_8 = 0;
  const SORT_12 var_14 = 0;
  const SORT_1 var_18 = 1;
  const SORT_1 var_22 = 0;
  // Collecting input declarations ...
  SORT_1 input_2;
  SORT_3 input_4;
  SORT_1 input_5;
  SORT_1 input_6;
  SORT_1 input_25;
  SORT_1 input_27;
  SORT_1 input_29;
  SORT_7 input_31;
  SORT_1 input_33;
  SORT_1 input_35;
  SORT_1 input_37;
  SORT_1 input_39;
  SORT_1 input_41;
  SORT_1 input_43;
  SORT_1 input_45;
  SORT_1 input_47;
  SORT_3 input_49;
  SORT_1 input_52;
  SORT_1 input_54;
  SORT_1 input_56;
  SORT_1 input_58;
  SORT_1 input_60;
  SORT_1 input_62;
  SORT_1 input_64;
  SORT_66 input_67;
  SORT_1 input_69;
  // Collecting state declarations ...
  SORT_7 state_9 = __VERIFIER_nondet_uchar() & mask_SORT_7;
  SORT_1 state_23 = __VERIFIER_nondet_uchar() & mask_SORT_1;
  // Initializing states ...
  SORT_7 init_10_arg_1 = var_8;
  state_9 = init_10_arg_1;
  SORT_1 init_24_arg_1 = var_22;
  state_23 = init_24_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_25 = __VERIFIER_nondet_uchar();
    input_25 = input_25 & mask_SORT_1;
    input_27 = __VERIFIER_nondet_uchar();
    input_27 = input_27 & mask_SORT_1;
    input_29 = __VERIFIER_nondet_uchar();
    input_29 = input_29 & mask_SORT_1;
    input_31 = __VERIFIER_nondet_uchar();
    input_31 = input_31 & mask_SORT_7;
    input_33 = __VERIFIER_nondet_uchar();
    input_33 = input_33 & mask_SORT_1;
    input_35 = __VERIFIER_nondet_uchar();
    input_35 = input_35 & mask_SORT_1;
    input_37 = __VERIFIER_nondet_uchar();
    input_37 = input_37 & mask_SORT_1;
    input_39 = __VERIFIER_nondet_uchar();
    input_39 = input_39 & mask_SORT_1;
    input_41 = __VERIFIER_nondet_uchar();
    input_41 = input_41 & mask_SORT_1;
    input_43 = __VERIFIER_nondet_uchar();
    input_43 = input_43 & mask_SORT_1;
    input_45 = __VERIFIER_nondet_uchar();
    input_45 = input_45 & mask_SORT_1;
    input_47 = __VERIFIER_nondet_uchar();
    input_47 = input_47 & mask_SORT_1;
    input_49 = __VERIFIER_nondet_uchar();
    input_49 = input_49 & mask_SORT_3;
    input_52 = __VERIFIER_nondet_uchar();
    input_52 = input_52 & mask_SORT_1;
    input_54 = __VERIFIER_nondet_uchar();
    input_54 = input_54 & mask_SORT_1;
    input_56 = __VERIFIER_nondet_uchar();
    input_56 = input_56 & mask_SORT_1;
    input_58 = __VERIFIER_nondet_uchar();
    input_58 = input_58 & mask_SORT_1;
    input_60 = __VERIFIER_nondet_uchar();
    input_60 = input_60 & mask_SORT_1;
    input_62 = __VERIFIER_nondet_uchar();
    input_62 = input_62 & mask_SORT_1;
    input_64 = __VERIFIER_nondet_uchar();
    input_64 = input_64 & mask_SORT_1;
    input_67 = __VERIFIER_nondet_ushort();
    input_67 = input_67 & mask_SORT_66;
    input_69 = __VERIFIER_nondet_uchar();
    input_69 = input_69 & mask_SORT_1;
    // Assuming invariants ...
    // Asserting properties ...
    SORT_7 var_11_arg_0 = state_9;
    SORT_1 var_11 = var_11_arg_0 >> 3;
    var_11 = var_11 & mask_SORT_1;
    SORT_1 var_13_arg_0 = var_11;
    SORT_12 var_13 = var_13_arg_0;
    SORT_12 var_15_arg_0 = var_13;
    SORT_12 var_15_arg_1 = var_14;
    SORT_1 var_15 = var_15_arg_0 == var_15_arg_1;
    SORT_1 var_19_arg_0 = var_15;
    SORT_1 var_19 = ~var_19_arg_0;
    var_19 = var_19 & mask_SORT_1;
    SORT_1 var_20_arg_0 = var_18;
    SORT_1 var_20_arg_1 = var_19;
    SORT_1 var_20 = var_20_arg_0 & var_20_arg_1;
    var_20 = var_20 & mask_SORT_1;
    SORT_1 bad_21_arg_0 = var_20;
    __VERIFIER_assert(!(bad_21_arg_0));
    // Computing next states ...
    SORT_1 var_71_arg_0 = state_23;
    SORT_7 var_71_arg_1 = state_9;
    SORT_7 var_71_arg_2 = state_9;
    SORT_7 var_71 = var_71_arg_0 ? var_71_arg_1 : var_71_arg_2;
    SORT_7 next_72_arg_1 = var_71;
    SORT_1 var_73_arg_0 = state_23;
    SORT_1 var_73_arg_1 = var_22;
    SORT_1 var_73_arg_2 = var_18;
    SORT_1 var_73 = var_73_arg_0 ? var_73_arg_1 : var_73_arg_2;
    SORT_1 next_74_arg_1 = var_73;
    // Assigning next states ...
    state_9 = next_72_arg_1;
    state_23 = next_74_arg_1;
  }
  return 0;
}