// 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", "vis_QF_BV_rotate32.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 5 bits
  const SORT_1 mask_SORT_1 = (SORT_1)-1 >> (sizeof(SORT_1) * 8 - 5);
  const SORT_1 msb_SORT_1 = (SORT_1)1 << (5 - 1);
  typedef unsigned char SORT_3;  // BV with 1 bits
  const SORT_3 mask_SORT_3 = (SORT_3)-1 >> (sizeof(SORT_3) * 8 - 1);
  const SORT_3 msb_SORT_3 = (SORT_3)1 << (1 - 1);
  typedef unsigned int SORT_5;  // BV with 32 bits
  const SORT_5 mask_SORT_5 = (SORT_5)-1 >> (sizeof(SORT_5) * 8 - 32);
  const SORT_5 msb_SORT_5 = (SORT_5)1 << (32 - 1);
  typedef unsigned int SORT_22;  // BV with 31 bits
  const SORT_22 mask_SORT_22 = (SORT_22)-1 >> (sizeof(SORT_22) * 8 - 31);
  const SORT_22 msb_SORT_22 = (SORT_22)1 << (31 - 1);
  typedef unsigned int SORT_29;  // BV with 30 bits
  const SORT_29 mask_SORT_29 = (SORT_29)-1 >> (sizeof(SORT_29) * 8 - 30);
  const SORT_29 msb_SORT_29 = (SORT_29)1 << (30 - 1);
  typedef unsigned char SORT_31;  // BV with 2 bits
  const SORT_31 mask_SORT_31 = (SORT_31)-1 >> (sizeof(SORT_31) * 8 - 2);
  const SORT_31 msb_SORT_31 = (SORT_31)1 << (2 - 1);
  typedef unsigned int SORT_37;  // BV with 28 bits
  const SORT_37 mask_SORT_37 = (SORT_37)-1 >> (sizeof(SORT_37) * 8 - 28);
  const SORT_37 msb_SORT_37 = (SORT_37)1 << (28 - 1);
  typedef unsigned char SORT_39;  // BV with 4 bits
  const SORT_39 mask_SORT_39 = (SORT_39)-1 >> (sizeof(SORT_39) * 8 - 4);
  const SORT_39 msb_SORT_39 = (SORT_39)1 << (4 - 1);
  typedef unsigned int SORT_45;  // BV with 24 bits
  const SORT_45 mask_SORT_45 = (SORT_45)-1 >> (sizeof(SORT_45) * 8 - 24);
  const SORT_45 msb_SORT_45 = (SORT_45)1 << (24 - 1);
  typedef unsigned char SORT_47;  // BV with 8 bits
  const SORT_47 mask_SORT_47 = (SORT_47)-1 >> (sizeof(SORT_47) * 8 - 8);
  const SORT_47 msb_SORT_47 = (SORT_47)1 << (8 - 1);
  typedef unsigned short SORT_53;  // BV with 16 bits
  const SORT_53 mask_SORT_53 = (SORT_53)-1 >> (sizeof(SORT_53) * 8 - 16);
  const SORT_53 msb_SORT_53 = (SORT_53)1 << (16 - 1);
  // Initializing constants ...
  const SORT_5 var_7 = 0;
  const SORT_5 var_10 = 2863311530;
  const SORT_3 var_15 = 1;
  // Collecting input declarations ...
  SORT_1 input_2;
  SORT_3 input_4;
  SORT_5 input_6;
  // Collecting state declarations ...
  SORT_5 state_8 = __VERIFIER_nondet_uint() & mask_SORT_5;
  SORT_5 state_19 = __VERIFIER_nondet_uint() & mask_SORT_5;
  // Initializing states ...
  SORT_5 init_9_arg_1 = var_7;
  state_8 = init_9_arg_1;
  SORT_5 init_20_arg_1 = var_7;
  state_19 = init_20_arg_1;
  for (;;) {
    // Getting external input values ...
    input_2 = __VERIFIER_nondet_uchar();
    input_4 = __VERIFIER_nondet_uchar();
    input_6 = __VERIFIER_nondet_uint();
    // Assuming invariants ...
    // Asserting properties ...
    SORT_5 var_11_arg_0 = state_8;
    SORT_5 var_11_arg_1 = var_10;
    SORT_3 var_11 = var_11_arg_0 == var_11_arg_1;
    SORT_3 var_12_arg_0 = var_11;
    SORT_3 var_12 = ~var_12_arg_0;
    SORT_3 var_16_arg_0 = var_12;
    SORT_3 var_16 = ~var_16_arg_0;
    SORT_3 var_17_arg_0 = var_15;
    SORT_3 var_17_arg_1 = var_16;
    SORT_3 var_17 = var_17_arg_0 & var_17_arg_1;
    var_17 = var_17 & mask_SORT_3;
    SORT_3 bad_18_arg_0 = var_17;
    __VERIFIER_assert(!(bad_18_arg_0));
    // Computing next states ...
    SORT_1 var_57_arg_0 = input_2;
    SORT_3 var_57 = var_57_arg_0 >> 4;
    var_57 = var_57 & mask_SORT_3;
    SORT_1 var_50_arg_0 = input_2;
    SORT_3 var_50 = var_50_arg_0 >> 3;
    var_50 = var_50 & mask_SORT_3;
    SORT_1 var_42_arg_0 = input_2;
    SORT_3 var_42 = var_42_arg_0 >> 2;
    var_42 = var_42 & mask_SORT_3;
    SORT_1 var_34_arg_0 = input_2;
    SORT_3 var_34 = var_34_arg_0 >> 1;
    var_34 = var_34 & mask_SORT_3;
    SORT_1 var_26_arg_0 = input_2;
    SORT_3 var_26 = var_26_arg_0 >> 0;
    var_26 = var_26 & mask_SORT_3;
    SORT_5 var_24_arg_0 = state_19;
    SORT_3 var_24 = var_24_arg_0 >> 0;
    SORT_5 var_23_arg_0 = state_19;
    SORT_22 var_23 = var_23_arg_0 >> 1;
    var_23 = var_23 & mask_SORT_22;
    SORT_3 var_25_arg_0 = var_24;
    SORT_22 var_25_arg_1 = var_23;
    SORT_5 var_25 = ((SORT_5)var_25_arg_0 << 31) | var_25_arg_1;
    SORT_3 var_27_arg_0 = var_26;
    SORT_5 var_27_arg_1 = var_25;
    SORT_5 var_27_arg_2 = state_19;
    SORT_5 var_27 = var_27_arg_0 ? var_27_arg_1 : var_27_arg_2;
    SORT_5 var_32_arg_0 = var_27;
    SORT_31 var_32 = var_32_arg_0 >> 0;
    SORT_5 var_30_arg_0 = var_27;
    SORT_29 var_30 = var_30_arg_0 >> 2;
    var_30 = var_30 & mask_SORT_29;
    SORT_31 var_33_arg_0 = var_32;
    SORT_29 var_33_arg_1 = var_30;
    SORT_5 var_33 = ((SORT_5)var_33_arg_0 << 30) | var_33_arg_1;
    SORT_3 var_35_arg_0 = var_34;
    SORT_5 var_35_arg_1 = var_33;
    SORT_5 var_35_arg_2 = var_27;
    SORT_5 var_35 = var_35_arg_0 ? var_35_arg_1 : var_35_arg_2;
    SORT_5 var_40_arg_0 = var_35;
    SORT_39 var_40 = var_40_arg_0 >> 0;
    SORT_5 var_38_arg_0 = var_35;
    SORT_37 var_38 = var_38_arg_0 >> 4;
    var_38 = var_38 & mask_SORT_37;
    SORT_39 var_41_arg_0 = var_40;
    SORT_37 var_41_arg_1 = var_38;
    SORT_5 var_41 = ((SORT_5)var_41_arg_0 << 28) | var_41_arg_1;
    SORT_3 var_43_arg_0 = var_42;
    SORT_5 var_43_arg_1 = var_41;
    SORT_5 var_43_arg_2 = var_35;
    SORT_5 var_43 = var_43_arg_0 ? var_43_arg_1 : var_43_arg_2;
    SORT_5 var_48_arg_0 = var_43;
    SORT_47 var_48 = var_48_arg_0 >> 0;
    SORT_5 var_46_arg_0 = var_43;
    SORT_45 var_46 = var_46_arg_0 >> 8;
    var_46 = var_46 & mask_SORT_45;
    SORT_47 var_49_arg_0 = var_48;
    SORT_45 var_49_arg_1 = var_46;
    SORT_5 var_49 = ((SORT_5)var_49_arg_0 << 24) | var_49_arg_1;
    SORT_3 var_51_arg_0 = var_50;
    SORT_5 var_51_arg_1 = var_49;
    SORT_5 var_51_arg_2 = var_43;
    SORT_5 var_51 = var_51_arg_0 ? var_51_arg_1 : var_51_arg_2;
    SORT_5 var_55_arg_0 = var_51;
    SORT_53 var_55 = var_55_arg_0 >> 0;
    SORT_5 var_54_arg_0 = var_51;
    SORT_53 var_54 = var_54_arg_0 >> 16;
    var_54 = var_54 & mask_SORT_53;
    SORT_53 var_56_arg_0 = var_55;
    SORT_53 var_56_arg_1 = var_54;
    SORT_5 var_56 = ((SORT_5)var_56_arg_0 << 16) | var_56_arg_1;
    SORT_3 var_58_arg_0 = var_57;
    SORT_5 var_58_arg_1 = var_56;
    SORT_5 var_58_arg_2 = var_51;
    SORT_5 var_58 = var_58_arg_0 ? var_58_arg_1 : var_58_arg_2;
    var_58 = var_58 & mask_SORT_5;
    SORT_5 next_60_arg_1 = var_58;
    SORT_5 next_61_arg_1 = input_6;
    // Assigning next states ...
    state_8 = next_60_arg_1;
    state_19 = next_61_arg_1;
  }
  return 0;
}