// 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", "bit-vector.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 3 bits
  const SORT_3 mask_SORT_3 = (SORT_3)-1 >> (sizeof(SORT_3) * 8 - 3);
  const SORT_3 msb_SORT_3 = (SORT_3)1 << (3 - 1);
  typedef unsigned int SORT_7;  // BV with 32 bits
  const SORT_7 mask_SORT_7 = (SORT_7)-1 >> (sizeof(SORT_7) * 8 - 32);
  const SORT_7 msb_SORT_7 = (SORT_7)1 << (32 - 1);
  typedef unsigned char SORT_21;  // BV with 2 bits
  const SORT_21 mask_SORT_21 = (SORT_21)-1 >> (sizeof(SORT_21) * 8 - 2);
  const SORT_21 msb_SORT_21 = (SORT_21)1 << (2 - 1);
  // Initializing constants ...
  const SORT_3 var_4 = 2;
  const SORT_7 var_9 = 2;
  const SORT_1 var_13 = 1;
  const SORT_3 var_17 = 6;
  // Collecting input declarations ...
  SORT_1 input_2;
  // Collecting state declarations ...
  SORT_3 state_5 = __VERIFIER_nondet_uchar() & mask_SORT_3;
  SORT_3 state_18 = __VERIFIER_nondet_uchar() & mask_SORT_3;
  // Initializing states ...
  SORT_3 init_6_arg_1 = var_4;
  state_5 = init_6_arg_1;
  SORT_3 init_19_arg_1 = var_17;
  state_18 = init_19_arg_1;
  for (;;) {
    // Getting external input values ...
    input_2 = __VERIFIER_nondet_uchar();
    // Assuming invariants ...
    // Asserting properties ...
    SORT_3 var_8_arg_0 = state_5;
    var_8_arg_0 = var_8_arg_0 & mask_SORT_3;
    SORT_7 var_8 = var_8_arg_0;
    SORT_7 var_10_arg_0 = var_8;
    SORT_7 var_10_arg_1 = var_9;
    SORT_1 var_10 = var_10_arg_0 >= var_10_arg_1;
    SORT_1 var_14_arg_0 = var_10;
    SORT_1 var_14 = ~var_14_arg_0;
    SORT_1 var_15_arg_0 = var_13;
    SORT_1 var_15_arg_1 = var_14;
    SORT_1 var_15 = var_15_arg_0 & var_15_arg_1;
    var_15 = var_15 & mask_SORT_1;
    SORT_1 bad_16_arg_0 = var_15;
    __VERIFIER_assert(!(bad_16_arg_0));
    // Computing next states ...
    SORT_3 var_23_arg_0 = state_18;
    SORT_1 var_23 = var_23_arg_0 >> 0;
    SORT_3 var_22_arg_0 = state_18;
    SORT_21 var_22 = var_22_arg_0 >> 1;
    var_22 = var_22 & mask_SORT_21;
    SORT_1 var_24_arg_0 = var_23;
    SORT_21 var_24_arg_1 = var_22;
    SORT_3 var_24 = ((SORT_3)var_24_arg_0 << 2) | var_24_arg_1;
    SORT_3 next_25_arg_1 = var_24;
    SORT_3 var_27_arg_0 = state_5;
    SORT_21 var_27 = var_27_arg_0 >> 0;
    SORT_3 var_26_arg_0 = state_5;
    SORT_1 var_26 = var_26_arg_0 >> 2;
    var_26 = var_26 & mask_SORT_1;
    SORT_21 var_28_arg_0 = var_27;
    SORT_1 var_28_arg_1 = var_26;
    SORT_3 var_28 = ((SORT_3)var_28_arg_0 << 1) | var_28_arg_1;
    SORT_3 next_29_arg_1 = var_28;
    // Assigning next states ...
    state_5 = next_25_arg_1;
    state_18 = next_29_arg_1;
  }
  return 0;
}