- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 5865356a-ff3e-466d-bbef-cbb19d264d2c
    creation_time: 2025-03-21T01:25:13Z
    producer:
      name: Goblint
      version: heads/master-0-g66dff5a90-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp.json'' ''--disable'' ''witness.graphml.enabled''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/valid-memsafety.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_nondet_insert-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_nondet_insert-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_nondet_insert-2.i: 5bf92ba2f935aadbe2c0ae3d366f72b4144ff6b8b5ce7c503e628d249b478be5
      data_model: ILP32
      language: C
      specification: 'CHECK( init(main()), LTL(G valid-free) )

        CHECK( init(main()), LTL(G valid-deref) )

        CHECK( init(main()), LTL(G valid-memtrack) )'
  content:
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_nondet_insert-2.i
        line: 588
        column: 3
        function: sll_length
      value: ((((((4 <= len || (head == 0 && len == 4)) || 4 <= len) || 4 <= len)
        || len == 3) || len == 2) || len == 1) || (0 == len && len == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_nondet_insert-2.i
        line: 621
        column: 3
        function: _get_nondet_int
      value: ((((((-1LL - (long long )from) + (long long )len >= 0LL && (1LL + (long
        long )from) - (long long )len >= 0LL) && ((((((((((((((-8LL + (long long )len)
        + (long long )until >= 0LL && (-7LL + (long long )from) + (long long )until
        >= 0LL) && (7LL - (long long )from) - (long long )until >= 0LL) && (8LL -
        (long long )len) - (long long )until >= 0LL) && ((((((((((((-5LL + (long long
        )from) + (long long )len >= 0LL && (-3LL - (long long )from) + (long long
        )until >= 0LL) && (-2LL - (long long )len) + (long long )until >= 0LL) &&
        (2LL + (long long )len) - (long long )until >= 0LL) && (3LL + (long long )from)
        - (long long )until >= 0LL) && (5LL - (long long )from) - (long long )len
        >= 0LL) && 2 == from) && 5 == until) && from == 2) && until == 5) && len ==
        3) || ((((((((((-1LL + (long long )from) + (long long )len >= 0LL && (-7LL
        - (long long )from) + (long long )until >= 0LL) && (-6LL - (long long )len)
        + (long long )until >= 0LL) && (6LL + (long long )len) - (long long )until
        >= 0LL) && (7LL + (long long )from) - (long long )until >= 0LL) && (1LL -
        (long long )from) - (long long )len >= 0LL) && 0 == from) && from == 0) &&
        until == 7) && len == 1))) || ((((((((((((((-7LL + (long long )len) + (long
        long )until >= 0LL && (-6LL + (long long )from) + (long long )until >= 0LL)
        && (-1LL + (long long )from) + (long long )len >= 0LL) && (-6LL - (long long
        )from) + (long long )until >= 0LL) && (-5LL - (long long )len) + (long long
        )until >= 0LL) && (5LL + (long long )len) - (long long )until >= 0LL) && (6LL
        + (long long )from) - (long long )until >= 0LL) && (1LL - (long long )from)
        - (long long )len >= 0LL) && (6LL - (long long )from) - (long long )until
        >= 0LL) && (7LL - (long long )len) - (long long )until >= 0LL) && 0 == from)
        && from == 0) && until == 6) && len == 1)) || ((((((((((((((-6LL + (long long
        )len) + (long long )until >= 0LL && (-5LL + (long long )from) + (long long
        )until >= 0LL) && (-1LL + (long long )from) + (long long )len >= 0LL) && (-5LL
        - (long long )from) + (long long )until >= 0LL) && (-4LL - (long long )len)
        + (long long )until >= 0LL) && (4LL + (long long )len) - (long long )until
        >= 0LL) && (5LL + (long long )from) - (long long )until >= 0LL) && (1LL -
        (long long )from) - (long long )len >= 0LL) && (5LL - (long long )from) -
        (long long )until >= 0LL) && (6LL - (long long )len) - (long long )until >=
        0LL) && 0 == from) && from == 0) && until == 5) && len == 1)) || ((((((((((((((-6LL
        + (long long )len) + (long long )until >= 0LL && (-5LL + (long long )from)
        + (long long )until >= 0LL) && (-1LL + (long long )from) + (long long )len
        >= 0LL) && (-5LL - (long long )from) + (long long )until >= 0LL) && (-4LL
        - (long long )len) + (long long )until >= 0LL) && (4LL + (long long )len)
        - (long long )until >= 0LL) && (5LL + (long long )from) - (long long )until
        >= 0LL) && (1LL - (long long )from) - (long long )len >= 0LL) && (5LL - (long
        long )from) - (long long )until >= 0LL) && (6LL - (long long )len) - (long
        long )until >= 0LL) && 0 == from) && from == 0) && until == 5) && len == 1))
        || ((((((((((((((-5LL + (long long )len) + (long long )until >= 0LL && (-4LL
        + (long long )from) + (long long )until >= 0LL) && (-1LL + (long long )from)
        + (long long )len >= 0LL) && (-4LL - (long long )from) + (long long )until
        >= 0LL) && (-3LL - (long long )len) + (long long )until >= 0LL) && (3LL +
        (long long )len) - (long long )until >= 0LL) && (4LL + (long long )from) -
        (long long )until >= 0LL) && (1LL - (long long )from) - (long long )len >=
        0LL) && (4LL - (long long )from) - (long long )until >= 0LL) && (5LL - (long
        long )len) - (long long )until >= 0LL) && 0 == from) && from == 0) && until
        == 4) && len == 1)) || ((((((((((((((-5LL + (long long )len) + (long long
        )until >= 0LL && (-4LL + (long long )from) + (long long )until >= 0LL) &&
        (-1LL + (long long )from) + (long long )len >= 0LL) && (-4LL - (long long
        )from) + (long long )until >= 0LL) && (-3LL - (long long )len) + (long long
        )until >= 0LL) && (3LL + (long long )len) - (long long )until >= 0LL) && (4LL
        + (long long )from) - (long long )until >= 0LL) && (1LL - (long long )from)
        - (long long )len >= 0LL) && (4LL - (long long )from) - (long long )until
        >= 0LL) && (5LL - (long long )len) - (long long )until >= 0LL) && 0 == from)
        && from == 0) && until == 4) && len == 1)) || ((((((((((((((-4LL + (long long
        )len) + (long long )until >= 0LL && (-3LL + (long long )from) + (long long
        )until >= 0LL) && (-1LL + (long long )from) + (long long )len >= 0LL) && (-3LL
        - (long long )from) + (long long )until >= 0LL) && (-2LL - (long long )len)
        + (long long )until >= 0LL) && (2LL + (long long )len) - (long long )until
        >= 0LL) && (3LL + (long long )from) - (long long )until >= 0LL) && (1LL -
        (long long )from) - (long long )len >= 0LL) && (3LL - (long long )from) -
        (long long )until >= 0LL) && (4LL - (long long )len) - (long long )until >=
        0LL) && 0 == from) && from == 0) && until == 3) && len == 1)) || ((((((((((((((-4LL
        + (long long )len) + (long long )until >= 0LL && (-3LL + (long long )from)
        + (long long )until >= 0LL) && (-1LL + (long long )from) + (long long )len
        >= 0LL) && (-3LL - (long long )from) + (long long )until >= 0LL) && (-2LL
        - (long long )len) + (long long )until >= 0LL) && (2LL + (long long )len)
        - (long long )until >= 0LL) && (3LL + (long long )from) - (long long )until
        >= 0LL) && (1LL - (long long )from) - (long long )len >= 0LL) && (3LL - (long
        long )from) - (long long )until >= 0LL) && (4LL - (long long )len) - (long
        long )until >= 0LL) && 0 == from) && from == 0) && until == 3) && len == 1))
        || ((((((((((((((-3LL + (long long )len) + (long long )until >= 0LL && (-2LL
        + (long long )from) + (long long )until >= 0LL) && (-1LL + (long long )from)
        + (long long )len >= 0LL) && (-2LL - (long long )from) + (long long )until
        >= 0LL) && (-1LL - (long long )len) + (long long )until >= 0LL) && (1LL +
        (long long )len) - (long long )until >= 0LL) && (2LL + (long long )from) -
        (long long )until >= 0LL) && (1LL - (long long )from) - (long long )len >=
        0LL) && (2LL - (long long )from) - (long long )until >= 0LL) && (3LL - (long
        long )len) - (long long )until >= 0LL) && 0 == from) && from == 0) && until
        == 2) && len == 1)) || ((((((((((((((-2LL + (long long )len) + (long long
        )until >= 0LL && (-1LL + (long long )from) + (long long )until >= 0LL) &&
        (-1LL + (long long )from) + (long long )len >= 0LL) && (-1LL - (long long
        )from) + (long long )until >= 0LL) && (0LL - (long long )len) + (long long
        )until >= 0LL) && (1LL + (long long )from) - (long long )until >= 0LL) &&
        (1LL - (long long )from) - (long long )until >= 0LL) && (1LL - (long long
        )from) - (long long )len >= 0LL) && (2LL - (long long )len) - (long long )until
        >= 0LL) && (long long )len - (long long )until >= 0LL) && 0 == from) && from
        == 0) && until == 1) && len == 1))) || ((((0LL - (long long )from) + (long
        long )len >= 0LL && (long long )from - (long long )len >= 0LL) && from ==
        len) && ((((((((((((((-7LL + (long long )from) + (long long )until >= 0LL
        && (-7LL + (long long )len) + (long long )until >= 0LL) && (7LL - (long long
        )from) - (long long )until >= 0LL) && (7LL - (long long )len) - (long long
        )until >= 0LL) && (((((((((((((-4LL + (long long )from) + (long long )len
        >= 0LL && (-3LL - (long long )from) + (long long )until >= 0LL) && (-3LL -
        (long long )len) + (long long )until >= 0LL) && (3LL + (long long )from) -
        (long long )until >= 0LL) && (3LL + (long long )len) - (long long )until >=
        0LL) && (4LL - (long long )from) - (long long )len >= 0LL) && 2 == from) &&
        2 == len) && 5 == until) && from == 2) && until == 5) && len == 2) || (((((((((((-7LL
        - (long long )from) + (long long )until >= 0LL && (-7LL - (long long )len)
        + (long long )until >= 0LL) && (long long )from + (long long )len >= 0LL)
        && (7LL + (long long )from) - (long long )until >= 0LL) && (7LL + (long long
        )len) - (long long )until >= 0LL) && (0LL - (long long )from) - (long long
        )len >= 0LL) && 0 == from) && 0 == len) && from == 0) && until == 7) && len
        == 0))) || (((((((((((((((-6LL + (long long )from) + (long long )until >=
        0LL && (-6LL + (long long )len) + (long long )until >= 0LL) && (-6LL - (long
        long )from) + (long long )until >= 0LL) && (-6LL - (long long )len) + (long
        long )until >= 0LL) && (long long )from + (long long )len >= 0LL) && (6LL
        + (long long )from) - (long long )until >= 0LL) && (6LL + (long long )len)
        - (long long )until >= 0LL) && (0LL - (long long )from) - (long long )len
        >= 0LL) && (6LL - (long long )from) - (long long )until >= 0LL) && (6LL -
        (long long )len) - (long long )until >= 0LL) && 0 == from) && 0 == len) &&
        from == 0) && until == 6) && len == 0)) || (((((((((((((((-5LL + (long long
        )from) + (long long )until >= 0LL && (-5LL + (long long )len) + (long long
        )until >= 0LL) && (-5LL - (long long )from) + (long long )until >= 0LL) &&
        (-5LL - (long long )len) + (long long )until >= 0LL) && (long long )from +
        (long long )len >= 0LL) && (5LL + (long long )from) - (long long )until >=
        0LL) && (5LL + (long long )len) - (long long )until >= 0LL) && (0LL - (long
        long )from) - (long long )len >= 0LL) && (5LL - (long long )from) - (long
        long )until >= 0LL) && (5LL - (long long )len) - (long long )until >= 0LL)
        && 0 == from) && 0 == len) && from == 0) && until == 5) && len == 0)) || (((((((((((((((-5LL
        + (long long )from) + (long long )until >= 0LL && (-5LL + (long long )len)
        + (long long )until >= 0LL) && (-5LL - (long long )from) + (long long )until
        >= 0LL) && (-5LL - (long long )len) + (long long )until >= 0LL) && (long long
        )from + (long long )len >= 0LL) && (5LL + (long long )from) - (long long )until
        >= 0LL) && (5LL + (long long )len) - (long long )until >= 0LL) && (0LL - (long
        long )from) - (long long )len >= 0LL) && (5LL - (long long )from) - (long
        long )until >= 0LL) && (5LL - (long long )len) - (long long )until >= 0LL)
        && 0 == from) && 0 == len) && from == 0) && until == 5) && len == 0)) || (((((((((((((((-4LL
        + (long long )from) + (long long )until >= 0LL && (-4LL + (long long )len)
        + (long long )until >= 0LL) && (-4LL - (long long )from) + (long long )until
        >= 0LL) && (-4LL - (long long )len) + (long long )until >= 0LL) && (long long
        )from + (long long )len >= 0LL) && (4LL + (long long )from) - (long long )until
        >= 0LL) && (4LL + (long long )len) - (long long )until >= 0LL) && (0LL - (long
        long )from) - (long long )len >= 0LL) && (4LL - (long long )from) - (long
        long )until >= 0LL) && (4LL - (long long )len) - (long long )until >= 0LL)
        && 0 == from) && 0 == len) && from == 0) && until == 4) && len == 0)) || (((((((((((((((-4LL
        + (long long )from) + (long long )until >= 0LL && (-4LL + (long long )len)
        + (long long )until >= 0LL) && (-4LL - (long long )from) + (long long )until
        >= 0LL) && (-4LL - (long long )len) + (long long )until >= 0LL) && (long long
        )from + (long long )len >= 0LL) && (4LL + (long long )from) - (long long )until
        >= 0LL) && (4LL + (long long )len) - (long long )until >= 0LL) && (0LL - (long
        long )from) - (long long )len >= 0LL) && (4LL - (long long )from) - (long
        long )until >= 0LL) && (4LL - (long long )len) - (long long )until >= 0LL)
        && 0 == from) && 0 == len) && from == 0) && until == 4) && len == 0)) || (((((((((((((((-3LL
        + (long long )from) + (long long )until >= 0LL && (-3LL + (long long )len)
        + (long long )until >= 0LL) && (-3LL - (long long )from) + (long long )until
        >= 0LL) && (-3LL - (long long )len) + (long long )until >= 0LL) && (long long
        )from + (long long )len >= 0LL) && (3LL + (long long )from) - (long long )until
        >= 0LL) && (3LL + (long long )len) - (long long )until >= 0LL) && (0LL - (long
        long )from) - (long long )len >= 0LL) && (3LL - (long long )from) - (long
        long )until >= 0LL) && (3LL - (long long )len) - (long long )until >= 0LL)
        && 0 == from) && 0 == len) && from == 0) && until == 3) && len == 0)) || (((((((((((((((-3LL
        + (long long )from) + (long long )until >= 0LL && (-3LL + (long long )len)
        + (long long )until >= 0LL) && (-3LL - (long long )from) + (long long )until
        >= 0LL) && (-3LL - (long long )len) + (long long )until >= 0LL) && (long long
        )from + (long long )len >= 0LL) && (3LL + (long long )from) - (long long )until
        >= 0LL) && (3LL + (long long )len) - (long long )until >= 0LL) && (0LL - (long
        long )from) - (long long )len >= 0LL) && (3LL - (long long )from) - (long
        long )until >= 0LL) && (3LL - (long long )len) - (long long )until >= 0LL)
        && 0 == from) && 0 == len) && from == 0) && until == 3) && len == 0)) || (((((((((((((((-2LL
        + (long long )from) + (long long )until >= 0LL && (-2LL + (long long )len)
        + (long long )until >= 0LL) && (-2LL - (long long )from) + (long long )until
        >= 0LL) && (-2LL - (long long )len) + (long long )until >= 0LL) && (long long
        )from + (long long )len >= 0LL) && (2LL + (long long )from) - (long long )until
        >= 0LL) && (2LL + (long long )len) - (long long )until >= 0LL) && (0LL - (long
        long )from) - (long long )len >= 0LL) && (2LL - (long long )from) - (long
        long )until >= 0LL) && (2LL - (long long )len) - (long long )until >= 0LL)
        && 0 == from) && 0 == len) && from == 0) && until == 2) && len == 0)) || (((((((((((((((-1LL
        + (long long )from) + (long long )until >= 0LL && (-1LL + (long long )len)
        + (long long )until >= 0LL) && (-1LL - (long long )from) + (long long )until
        >= 0LL) && (-1LL - (long long )len) + (long long )until >= 0LL) && (long long
        )from + (long long )len >= 0LL) && (1LL + (long long )from) - (long long )until
        >= 0LL) && (1LL + (long long )len) - (long long )until >= 0LL) && (0LL - (long
        long )from) - (long long )len >= 0LL) && (1LL - (long long )from) - (long
        long )until >= 0LL) && (1LL - (long long )len) - (long long )until >= 0LL)
        && 0 == from) && 0 == len) && from == 0) && until == 1) && len == 0)))) ||
        ((((((-4LL + (long long )from) + (long long )len >= 0LL && (-4LL - (long long
        )from) + (long long )len >= 0LL) && (0LL - (long long )len) + (long long )until
        >= 0LL) && 0 == from) && from == 0) && (((((4 <= len && (((((((((((len <=
        7 && (-11LL + (long long )len) + (long long )until >= 0LL) && (-7LL + (long
        long )from) + (long long )until >= 0LL) && (-7LL - (long long )from) + (long
        long )until >= 0LL) && (3LL + (long long )len) - (long long )until >= 0LL)
        && (7LL + (long long )from) - (long long )until >= 0LL) && (7LL + (long long
        )from) - (long long )len >= 0LL) && (7LL - (long long )from) - (long long
        )until >= 0LL) && (7LL - (long long )from) - (long long )len >= 0LL) && (14LL
        - (long long )len) - (long long )until >= 0LL) && until == 7) || ((((((((((len
        <= 6 && (-10LL + (long long )len) + (long long )until >= 0LL) && (-6LL + (long
        long )from) + (long long )until >= 0LL) && (-6LL - (long long )from) + (long
        long )until >= 0LL) && (2LL + (long long )len) - (long long )until >= 0LL)
        && (6LL + (long long )from) - (long long )until >= 0LL) && (6LL + (long long
        )from) - (long long )len >= 0LL) && (6LL - (long long )from) - (long long
        )until >= 0LL) && (6LL - (long long )from) - (long long )len >= 0LL) && (12LL
        - (long long )len) - (long long )until >= 0LL) && until == 6))) || (((((((((((-9LL
        + (long long )len) + (long long )until >= 0LL && (-5LL + (long long )from)
        + (long long )until >= 0LL) && (-5LL - (long long )from) + (long long )until
        >= 0LL) && (1LL + (long long )len) - (long long )until >= 0LL) && (5LL + (long
        long )from) - (long long )until >= 0LL) && (5LL + (long long )from) - (long
        long )len >= 0LL) && (5LL - (long long )from) - (long long )until >= 0LL)
        && (5LL - (long long )from) - (long long )len >= 0LL) && (10LL - (long long
        )len) - (long long )until >= 0LL) && until == 5) && (len == 4 || len == 5)))
        || (((((((((((-9LL + (long long )len) + (long long )until >= 0LL && (-5LL
        + (long long )from) + (long long )until >= 0LL) && (-5LL - (long long )from)
        + (long long )until >= 0LL) && (1LL + (long long )len) - (long long )until
        >= 0LL) && (5LL + (long long )from) - (long long )until >= 0LL) && (5LL +
        (long long )from) - (long long )len >= 0LL) && (5LL - (long long )from) -
        (long long )until >= 0LL) && (5LL - (long long )from) - (long long )len >=
        0LL) && (10LL - (long long )len) - (long long )until >= 0LL) && until == 5)
        && (len == 4 || len == 5))) || (((((((((((-8LL + (long long )len) + (long
        long )until >= 0LL && (-4LL + (long long )from) + (long long )until >= 0LL)
        && (-4LL - (long long )from) + (long long )until >= 0LL) && (4LL + (long long
        )from) - (long long )until >= 0LL) && (4LL + (long long )from) - (long long
        )len >= 0LL) && (4LL - (long long )from) - (long long )until >= 0LL) && (4LL
        - (long long )from) - (long long )len >= 0LL) && (8LL - (long long )len) -
        (long long )until >= 0LL) && (long long )len - (long long )until >= 0LL) &&
        until == 4) && len == 4)) || (((((((((((-8LL + (long long )len) + (long long
        )until >= 0LL && (-4LL + (long long )from) + (long long )until >= 0LL) &&
        (-4LL - (long long )from) + (long long )until >= 0LL) && (4LL + (long long
        )from) - (long long )until >= 0LL) && (4LL + (long long )from) - (long long
        )len >= 0LL) && (4LL - (long long )from) - (long long )until >= 0LL) && (4LL
        - (long long )from) - (long long )len >= 0LL) && (8LL - (long long )len) -
        (long long )until >= 0LL) && (long long )len - (long long )until >= 0LL) &&
        until == 4) && len == 4)))) || (((-3LL - (long long )from) + (long long )len
        >= 0LL && (3LL + (long long )from) - (long long )len >= 0LL) && ((((((((((((-10LL
        + (long long )len) + (long long )until >= 0LL && (-7LL + (long long )from)
        + (long long )until >= 0LL) && (7LL - (long long )from) - (long long )until
        >= 0LL) && (10LL - (long long )len) - (long long )until >= 0LL) && ((((((((((((-7LL
        + (long long )from) + (long long )len >= 0LL && (-3LL - (long long )from)
        + (long long )until >= 0LL) && (0LL - (long long )len) + (long long )until
        >= 0LL) && (3LL + (long long )from) - (long long )until >= 0LL) && (7LL -
        (long long )from) - (long long )len >= 0LL) && (long long )len - (long long
        )until >= 0LL) && 2 == from) && 5 == until) && from == 2) && until == 5) &&
        len == 5) || ((((((((((-3LL + (long long )from) + (long long )len >= 0LL &&
        (-7LL - (long long )from) + (long long )until >= 0LL) && (-4LL - (long long
        )len) + (long long )until >= 0LL) && (4LL + (long long )len) - (long long
        )until >= 0LL) && (7LL + (long long )from) - (long long )until >= 0LL) &&
        (3LL - (long long )from) - (long long )len >= 0LL) && 0 == from) && from ==
        0) && until == 7) && len == 3))) || ((((((((((((((-9LL + (long long )len)
        + (long long )until >= 0LL && (-6LL + (long long )from) + (long long )until
        >= 0LL) && (-3LL + (long long )from) + (long long )len >= 0LL) && (-6LL -
        (long long )from) + (long long )until >= 0LL) && (-3LL - (long long )len)
        + (long long )until >= 0LL) && (3LL + (long long )len) - (long long )until
        >= 0LL) && (6LL + (long long )from) - (long long )until >= 0LL) && (3LL -
        (long long )from) - (long long )len >= 0LL) && (6LL - (long long )from) -
        (long long )until >= 0LL) && (9LL - (long long )len) - (long long )until >=
        0LL) && 0 == from) && from == 0) && until == 6) && len == 3)) || ((((((((((((((-8LL
        + (long long )len) + (long long )until >= 0LL && (-5LL + (long long )from)
        + (long long )until >= 0LL) && (-3LL + (long long )from) + (long long )len
        >= 0LL) && (-5LL - (long long )from) + (long long )until >= 0LL) && (-2LL
        - (long long )len) + (long long )until >= 0LL) && (2LL + (long long )len)
        - (long long )until >= 0LL) && (5LL + (long long )from) - (long long )until
        >= 0LL) && (3LL - (long long )from) - (long long )len >= 0LL) && (5LL - (long
        long )from) - (long long )until >= 0LL) && (8LL - (long long )len) - (long
        long )until >= 0LL) && 0 == from) && from == 0) && until == 5) && len == 3))
        || ((((((((((((((-8LL + (long long )len) + (long long )until >= 0LL && (-5LL
        + (long long )from) + (long long )until >= 0LL) && (-3LL + (long long )from)
        + (long long )len >= 0LL) && (-5LL - (long long )from) + (long long )until
        >= 0LL) && (-2LL - (long long )len) + (long long )until >= 0LL) && (2LL +
        (long long )len) - (long long )until >= 0LL) && (5LL + (long long )from) -
        (long long )until >= 0LL) && (3LL - (long long )from) - (long long )len >=
        0LL) && (5LL - (long long )from) - (long long )until >= 0LL) && (8LL - (long
        long )len) - (long long )until >= 0LL) && 0 == from) && from == 0) && until
        == 5) && len == 3)) || ((((((((((((((-7LL + (long long )len) + (long long
        )until >= 0LL && (-4LL + (long long )from) + (long long )until >= 0LL) &&
        (-3LL + (long long )from) + (long long )len >= 0LL) && (-4LL - (long long
        )from) + (long long )until >= 0LL) && (-1LL - (long long )len) + (long long
        )until >= 0LL) && (1LL + (long long )len) - (long long )until >= 0LL) && (4LL
        + (long long )from) - (long long )until >= 0LL) && (3LL - (long long )from)
        - (long long )len >= 0LL) && (4LL - (long long )from) - (long long )until
        >= 0LL) && (7LL - (long long )len) - (long long )until >= 0LL) && 0 == from)
        && from == 0) && until == 4) && len == 3)) || ((((((((((((((-7LL + (long long
        )len) + (long long )until >= 0LL && (-4LL + (long long )from) + (long long
        )until >= 0LL) && (-3LL + (long long )from) + (long long )len >= 0LL) && (-4LL
        - (long long )from) + (long long )until >= 0LL) && (-1LL - (long long )len)
        + (long long )until >= 0LL) && (1LL + (long long )len) - (long long )until
        >= 0LL) && (4LL + (long long )from) - (long long )until >= 0LL) && (3LL -
        (long long )from) - (long long )len >= 0LL) && (4LL - (long long )from) -
        (long long )until >= 0LL) && (7LL - (long long )len) - (long long )until >=
        0LL) && 0 == from) && from == 0) && until == 4) && len == 3)) || ((((((((((((((-6LL
        + (long long )len) + (long long )until >= 0LL && (-3LL + (long long )from)
        + (long long )until >= 0LL) && (-3LL + (long long )from) + (long long )len
        >= 0LL) && (-3LL - (long long )from) + (long long )until >= 0LL) && (0LL -
        (long long )len) + (long long )until >= 0LL) && (3LL + (long long )from) -
        (long long )until >= 0LL) && (3LL - (long long )from) - (long long )until
        >= 0LL) && (3LL - (long long )from) - (long long )len >= 0LL) && (6LL - (long
        long )len) - (long long )until >= 0LL) && (long long )len - (long long )until
        >= 0LL) && 0 == from) && from == 0) && until == 3) && len == 3)) || ((((((((((((((-6LL
        + (long long )len) + (long long )until >= 0LL && (-3LL + (long long )from)
        + (long long )until >= 0LL) && (-3LL + (long long )from) + (long long )len
        >= 0LL) && (-3LL - (long long )from) + (long long )until >= 0LL) && (0LL -
        (long long )len) + (long long )until >= 0LL) && (3LL + (long long )from) -
        (long long )until >= 0LL) && (3LL - (long long )from) - (long long )until
        >= 0LL) && (3LL - (long long )from) - (long long )len >= 0LL) && (6LL - (long
        long )len) - (long long )until >= 0LL) && (long long )len - (long long )until
        >= 0LL) && 0 == from) && from == 0) && until == 3) && len == 3)))) || (((-2LL
        - (long long )from) + (long long )len >= 0LL && (2LL + (long long )from) -
        (long long )len >= 0LL) && (((((((((((((-9LL + (long long )len) + (long long
        )until >= 0LL && (-7LL + (long long )from) + (long long )until >= 0LL) &&
        (7LL - (long long )from) - (long long )until >= 0LL) && (9LL - (long long
        )len) - (long long )until >= 0LL) && ((((((((((((-6LL + (long long )from)
        + (long long )len >= 0LL && (-3LL - (long long )from) + (long long )until
        >= 0LL) && (-1LL - (long long )len) + (long long )until >= 0LL) && (1LL +
        (long long )len) - (long long )until >= 0LL) && (3LL + (long long )from) -
        (long long )until >= 0LL) && (6LL - (long long )from) - (long long )len >=
        0LL) && 2 == from) && 5 == until) && from == 2) && until == 5) && len == 4)
        || ((((((((((-2LL + (long long )from) + (long long )len >= 0LL && (-7LL -
        (long long )from) + (long long )until >= 0LL) && (-5LL - (long long )len)
        + (long long )until >= 0LL) && (5LL + (long long )len) - (long long )until
        >= 0LL) && (7LL + (long long )from) - (long long )until >= 0LL) && (2LL -
        (long long )from) - (long long )len >= 0LL) && 0 == from) && from == 0) &&
        until == 7) && len == 2))) || ((((((((((((((-8LL + (long long )len) + (long
        long )until >= 0LL && (-6LL + (long long )from) + (long long )until >= 0LL)
        && (-2LL + (long long )from) + (long long )len >= 0LL) && (-6LL - (long long
        )from) + (long long )until >= 0LL) && (-4LL - (long long )len) + (long long
        )until >= 0LL) && (4LL + (long long )len) - (long long )until >= 0LL) && (6LL
        + (long long )from) - (long long )until >= 0LL) && (2LL - (long long )from)
        - (long long )len >= 0LL) && (6LL - (long long )from) - (long long )until
        >= 0LL) && (8LL - (long long )len) - (long long )until >= 0LL) && 0 == from)
        && from == 0) && until == 6) && len == 2)) || ((((((((((((((-7LL + (long long
        )len) + (long long )until >= 0LL && (-5LL + (long long )from) + (long long
        )until >= 0LL) && (-2LL + (long long )from) + (long long )len >= 0LL) && (-5LL
        - (long long )from) + (long long )until >= 0LL) && (-3LL - (long long )len)
        + (long long )until >= 0LL) && (3LL + (long long )len) - (long long )until
        >= 0LL) && (5LL + (long long )from) - (long long )until >= 0LL) && (2LL -
        (long long )from) - (long long )len >= 0LL) && (5LL - (long long )from) -
        (long long )until >= 0LL) && (7LL - (long long )len) - (long long )until >=
        0LL) && 0 == from) && from == 0) && until == 5) && len == 2)) || ((((((((((((((-7LL
        + (long long )len) + (long long )until >= 0LL && (-5LL + (long long )from)
        + (long long )until >= 0LL) && (-2LL + (long long )from) + (long long )len
        >= 0LL) && (-5LL - (long long )from) + (long long )until >= 0LL) && (-3LL
        - (long long )len) + (long long )until >= 0LL) && (3LL + (long long )len)
        - (long long )until >= 0LL) && (5LL + (long long )from) - (long long )until
        >= 0LL) && (2LL - (long long )from) - (long long )len >= 0LL) && (5LL - (long
        long )from) - (long long )until >= 0LL) && (7LL - (long long )len) - (long
        long )until >= 0LL) && 0 == from) && from == 0) && until == 5) && len == 2))
        || ((((((((((((((-6LL + (long long )len) + (long long )until >= 0LL && (-4LL
        + (long long )from) + (long long )until >= 0LL) && (-2LL + (long long )from)
        + (long long )len >= 0LL) && (-4LL - (long long )from) + (long long )until
        >= 0LL) && (-2LL - (long long )len) + (long long )until >= 0LL) && (2LL +
        (long long )len) - (long long )until >= 0LL) && (4LL + (long long )from) -
        (long long )until >= 0LL) && (2LL - (long long )from) - (long long )len >=
        0LL) && (4LL - (long long )from) - (long long )until >= 0LL) && (6LL - (long
        long )len) - (long long )until >= 0LL) && 0 == from) && from == 0) && until
        == 4) && len == 2)) || ((((((((((((((-6LL + (long long )len) + (long long
        )until >= 0LL && (-4LL + (long long )from) + (long long )until >= 0LL) &&
        (-2LL + (long long )from) + (long long )len >= 0LL) && (-4LL - (long long
        )from) + (long long )until >= 0LL) && (-2LL - (long long )len) + (long long
        )until >= 0LL) && (2LL + (long long )len) - (long long )until >= 0LL) && (4LL
        + (long long )from) - (long long )until >= 0LL) && (2LL - (long long )from)
        - (long long )len >= 0LL) && (4LL - (long long )from) - (long long )until
        >= 0LL) && (6LL - (long long )len) - (long long )until >= 0LL) && 0 == from)
        && from == 0) && until == 4) && len == 2)) || ((((((((((((((-5LL + (long long
        )len) + (long long )until >= 0LL && (-3LL + (long long )from) + (long long
        )until >= 0LL) && (-2LL + (long long )from) + (long long )len >= 0LL) && (-3LL
        - (long long )from) + (long long )until >= 0LL) && (-1LL - (long long )len)
        + (long long )until >= 0LL) && (1LL + (long long )len) - (long long )until
        >= 0LL) && (3LL + (long long )from) - (long long )until >= 0LL) && (2LL -
        (long long )from) - (long long )len >= 0LL) && (3LL - (long long )from) -
        (long long )until >= 0LL) && (5LL - (long long )len) - (long long )until >=
        0LL) && 0 == from) && from == 0) && until == 3) && len == 2)) || ((((((((((((((-5LL
        + (long long )len) + (long long )until >= 0LL && (-3LL + (long long )from)
        + (long long )until >= 0LL) && (-2LL + (long long )from) + (long long )len
        >= 0LL) && (-3LL - (long long )from) + (long long )until >= 0LL) && (-1LL
        - (long long )len) + (long long )until >= 0LL) && (1LL + (long long )len)
        - (long long )until >= 0LL) && (3LL + (long long )from) - (long long )until
        >= 0LL) && (2LL - (long long )from) - (long long )len >= 0LL) && (3LL - (long
        long )from) - (long long )until >= 0LL) && (5LL - (long long )len) - (long
        long )until >= 0LL) && 0 == from) && from == 0) && until == 3) && len == 2))
        || ((((((((((((((-4LL + (long long )len) + (long long )until >= 0LL && (-2LL
        + (long long )from) + (long long )until >= 0LL) && (-2LL + (long long )from)
        + (long long )len >= 0LL) && (-2LL - (long long )from) + (long long )until
        >= 0LL) && (0LL - (long long )len) + (long long )until >= 0LL) && (2LL + (long
        long )from) - (long long )until >= 0LL) && (2LL - (long long )from) - (long
        long )until >= 0LL) && (2LL - (long long )from) - (long long )len >= 0LL)
        && (4LL - (long long )len) - (long long )until >= 0LL) && (long long )len
        - (long long )until >= 0LL) && 0 == from) && from == 0) && until == 2) &&
        len == 2)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_nondet_insert-2.i
        line: 608
        column: 3
        function: sll_insert
      value: (-1 <= position && ((((((((position <= 3 || position <= 2) || position
        <= 1) || position <= 1) || position <= 0) || position <= 0) || (((((((position
        <= 4 || position <= 3) || position <= 2) || position <= 2) || position <=
        1) || position <= 0) || position <= 1) || position <= 0)) || ((((((((position
        <= 5 || position <= 4) || position <= 3) || position <= 3) || position <=
        2) || position <= 1) || position <= 2) || position <= 1) || position <= 0))
        || (second_to_last == *head && (((((((((position <= 6 || position <= 5) ||
        position <= 4) || position <= 4) || position <= 3) || position <= 2) || position
        <= 3) || position <= 2) || position <= 1) || position <= 0)))) || (((0 ==
        second_to_last && second_to_last == 0) && last == *head) && (((((((((0 <=
        position && (position <= 7 || position <= 6)) || (((((position == 0 || position
        == 1) || position == 2) || position == 3) || position == 4) || position ==
        5)) || (((((position == 0 || position == 1) || position == 2) || position
        == 3) || position == 4) || position == 5)) || ((((position == 0 || position
        == 1) || position == 2) || position == 3) || position == 4)) || (((position
        == 0 || position == 1) || position == 2) || position == 3)) || ((((position
        == 0 || position == 1) || position == 2) || position == 3) || position ==
        4)) || (((position == 0 || position == 1) || position == 2) || position ==
        3)) || ((position == 0 || position == 1) || position == 2)) || (position ==
        0 || position == 1)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_nondet_insert-2.i
        line: 631
        column: 3
        function: main
      value: (((0LL - (long long )i) + (long long )k >= 0LL && (2147483647LL - (long
        long )k) + (long long )position >= 0LL) && ((((((((((((((((((((((((((((0 <=
        position && position <= 7) && (-9LL + (long long )k) + (long long )len >=
        0LL) && (-9LL + (long long )i) + (long long )len >= 0LL) && (-8LL + (long
        long )i) + (long long )k >= 0LL) && (-5LL + (long long )len) + (long long
        )position >= 0LL) && (-4LL + (long long )k) + (long long )position >= 0LL)
        && (-4LL + (long long )i) + (long long )position >= 0LL) && (-1LL - (long
        long )i) + (long long )len >= 0LL) && (4LL - (long long )i) + (long long )position
        >= 0LL) && (5LL - (long long )len) + (long long )position >= 0LL) && (2147483642LL
        - (long long )k) + (long long )len >= 0LL) && (1LL + (long long )k) - (long
        long )len >= 0LL) && (1LL + (long long )i) - (long long )len >= 0LL) && (2LL
        + (long long )len) - (long long )position >= 0LL) && (3LL + (long long )k)
        - (long long )position >= 0LL) && (3LL + (long long )i) - (long long )position
        >= 0LL) && (2147483643LL + (long long )i) - (long long )k >= 0LL) && (9LL
        - (long long )i) - (long long )len >= 0LL) && (11LL - (long long )i) - (long
        long )position >= 0LL) && (12LL - (long long )len) - (long long )position
        >= 0LL) && (2147483651LL - (long long )i) - (long long )k >= 0LL) && (2147483652LL
        - (long long )k) - (long long )len >= 0LL) && (2147483654LL - (long long )k)
        - (long long )position >= 0LL) && i == 4) && (int )k == 4) || (((((((((-6LL
        + (long long )i) + (long long )k >= 0LL && (-3LL + (long long )k) + (long
        long )position >= 0LL) && (-3LL + (long long )i) + (long long )position >=
        0LL) && (3LL - (long long )i) + (long long )position >= 0LL) && (1LL + (long
        long )len) - (long long )position >= 0LL) && (2147483644LL + (long long )i)
        - (long long )k >= 0LL) && (2147483650LL - (long long )i) - (long long )k
        >= 0LL) && i == 3) && ((((((((((((((((((0 <= position && position <= 6) &&
        (-8LL + (long long )k) + (long long )len >= 0LL) && (-8LL + (long long )i)
        + (long long )len >= 0LL) && (-5LL + (long long )len) + (long long )position
        >= 0LL) && (-2LL - (long long )i) + (long long )len >= 0LL) && (5LL - (long
        long )len) + (long long )position >= 0LL) && (2147483642LL - (long long )k)
        + (long long )len >= 0LL) && (2LL + (long long )k) - (long long )len >= 0LL)
        && (2LL + (long long )i) - (long long )len >= 0LL) && (3LL + (long long )k)
        - (long long )position >= 0LL) && (3LL + (long long )i) - (long long )position
        >= 0LL) && (8LL - (long long )i) - (long long )len >= 0LL) && (9LL - (long
        long )i) - (long long )position >= 0LL) && (11LL - (long long )len) - (long
        long )position >= 0LL) && (2147483652LL - (long long )k) - (long long )len
        >= 0LL) && (2147483653LL - (long long )k) - (long long )position >= 0LL) &&
        ((((int )k == 1 || (int )k == 2) || (int )k == 3) || (int )k == 4)) || (((((((((((((((((-7LL
        + (long long )k) + (long long )len >= 0LL && (-7LL + (long long )i) + (long
        long )len >= 0LL) && (-4LL + (long long )len) + (long long )position >= 0LL)
        && (-1LL - (long long )i) + (long long )len >= 0LL) && (4LL - (long long )len)
        + (long long )position >= 0LL) && (2147483643LL - (long long )k) + (long long
        )len >= 0LL) && (1LL + (long long )k) - (long long )len >= 0LL) && (1LL +
        (long long )i) - (long long )len >= 0LL) && (2LL + (long long )k) - (long
        long )position >= 0LL) && (2LL + (long long )i) - (long long )position >=
        0LL) && (7LL - (long long )i) - (long long )len >= 0LL) && (8LL - (long long
        )i) - (long long )position >= 0LL) && (9LL - (long long )len) - (long long
        )position >= 0LL) && (2147483651LL - (long long )k) - (long long )len >= 0LL)
        && (2147483652LL - (long long )k) - (long long )position >= 0LL) && (int )k
        == 3) && (((((position == 0 || position == 1) || position == 2) || position
        == 3) || position == 4) || position == 5))))) || (((((((((-4LL + (long long
        )i) + (long long )k >= 0LL && (-2LL + (long long )k) + (long long )position
        >= 0LL) && (-2LL + (long long )i) + (long long )position >= 0LL) && (2LL -
        (long long )i) + (long long )position >= 0LL) && (2147483645LL + (long long
        )i) - (long long )k >= 0LL) && (2147483649LL - (long long )i) - (long long
        )k >= 0LL) && (long long )len - (long long )position >= 0LL) && i == 2) &&
        (((((((((((((((((((-7LL + (long long )k) + (long long )len >= 0LL && (-7LL
        + (long long )i) + (long long )len >= 0LL) && (-5LL + (long long )len) + (long
        long )position >= 0LL) && (-3LL - (long long )i) + (long long )len >= 0LL)
        && (5LL - (long long )len) + (long long )position >= 0LL) && (2147483642LL
        - (long long )k) + (long long )len >= 0LL) && (3LL + (long long )k) - (long
        long )len >= 0LL) && (3LL + (long long )k) - (long long )position >= 0LL)
        && (3LL + (long long )i) - (long long )len >= 0LL) && (3LL + (long long )i)
        - (long long )position >= 0LL) && (7LL - (long long )i) - (long long )len
        >= 0LL) && (7LL - (long long )i) - (long long )position >= 0LL) && (10LL -
        (long long )len) - (long long )position >= 0LL) && (2147483652LL - (long long
        )k) - (long long )len >= 0LL) && (2147483652LL - (long long )k) - (long long
        )position >= 0LL) && ((((int )k == 1 || (int )k == 2) || (int )k == 3) ||
        (int )k == 4)) && (((((position == 0 || position == 1) || position == 2) ||
        position == 3) || position == 4) || position == 5)) || (((((((((((((((((-6LL
        + (long long )k) + (long long )len >= 0LL && (-6LL + (long long )i) + (long
        long )len >= 0LL) && (-4LL + (long long )len) + (long long )position >= 0LL)
        && (-2LL - (long long )i) + (long long )len >= 0LL) && (4LL - (long long )len)
        + (long long )position >= 0LL) && (2147483643LL - (long long )k) + (long long
        )len >= 0LL) && (2LL + (long long )k) - (long long )len >= 0LL) && (2LL +
        (long long )k) - (long long )position >= 0LL) && (2LL + (long long )i) - (long
        long )len >= 0LL) && (2LL + (long long )i) - (long long )position >= 0LL)
        && (6LL - (long long )i) - (long long )len >= 0LL) && (6LL - (long long )i)
        - (long long )position >= 0LL) && (8LL - (long long )len) - (long long )position
        >= 0LL) && (2147483651LL - (long long )k) - (long long )len >= 0LL) && (2147483651LL
        - (long long )k) - (long long )position >= 0LL) && (((int )k == 1 || (int
        )k == 2) || (int )k == 3)) && ((((position == 0 || position == 1) || position
        == 2) || position == 3) || position == 4))) || (((((((((((((((((-5LL + (long
        long )k) + (long long )len >= 0LL && (-5LL + (long long )i) + (long long )len
        >= 0LL) && (-3LL + (long long )len) + (long long )position >= 0LL) && (-1LL
        - (long long )i) + (long long )len >= 0LL) && (3LL - (long long )len) + (long
        long )position >= 0LL) && (2147483644LL - (long long )k) + (long long )len
        >= 0LL) && (1LL + (long long )k) - (long long )len >= 0LL) && (1LL + (long
        long )k) - (long long )position >= 0LL) && (1LL + (long long )i) - (long long
        )len >= 0LL) && (1LL + (long long )i) - (long long )position >= 0LL) && (5LL
        - (long long )i) - (long long )len >= 0LL) && (5LL - (long long )i) - (long
        long )position >= 0LL) && (6LL - (long long )len) - (long long )position >=
        0LL) && (2147483650LL - (long long )k) - (long long )len >= 0LL) && (2147483650LL
        - (long long )k) - (long long )position >= 0LL) && (int )k == 2) && (((position
        == 0 || position == 1) || position == 2) || position == 3))))) || (((((((((-2LL
        + (long long )i) + (long long )k >= 0LL && (-1LL + (long long )k) + (long
        long )position >= 0LL) && (-1LL + (long long )i) + (long long )position >=
        0LL) && (1LL - (long long )i) + (long long )position >= 0LL) && (-1LL + (long
        long )len) - (long long )position >= 0LL) && (2147483646LL + (long long )i)
        - (long long )k >= 0LL) && (2147483648LL - (long long )i) - (long long )k
        >= 0LL) && i == 1) && ((((((((((((((((((((-6LL + (long long )k) + (long long
        )len >= 0LL && (-6LL + (long long )i) + (long long )len >= 0LL) && (-5LL +
        (long long )len) + (long long )position >= 0LL) && (-4LL - (long long )i)
        + (long long )len >= 0LL) && (5LL - (long long )len) + (long long )position
        >= 0LL) && (2147483642LL - (long long )k) + (long long )len >= 0LL) && (3LL
        + (long long )k) - (long long )position >= 0LL) && (3LL + (long long )i) -
        (long long )position >= 0LL) && (4LL + (long long )k) - (long long )len >=
        0LL) && (4LL + (long long )i) - (long long )len >= 0LL) && (5LL - (long long
        )i) - (long long )position >= 0LL) && (6LL - (long long )i) - (long long )len
        >= 0LL) && (9LL - (long long )len) - (long long )position >= 0LL) && (2147483651LL
        - (long long )k) - (long long )position >= 0LL) && (2147483652LL - (long long
        )k) - (long long )len >= 0LL) && ((((int )k == 1 || (int )k == 2) || (int
        )k == 3) || (int )k == 4)) && ((((position == 0 || position == 1) || position
        == 2) || position == 3) || position == 4)) || (((((((((((((((((-5LL + (long
        long )k) + (long long )len >= 0LL && (-5LL + (long long )i) + (long long )len
        >= 0LL) && (-4LL + (long long )len) + (long long )position >= 0LL) && (-3LL
        - (long long )i) + (long long )len >= 0LL) && (4LL - (long long )len) + (long
        long )position >= 0LL) && (2147483643LL - (long long )k) + (long long )len
        >= 0LL) && (2LL + (long long )k) - (long long )position >= 0LL) && (2LL +
        (long long )i) - (long long )position >= 0LL) && (3LL + (long long )k) - (long
        long )len >= 0LL) && (3LL + (long long )i) - (long long )len >= 0LL) && (4LL
        - (long long )i) - (long long )position >= 0LL) && (5LL - (long long )i) -
        (long long )len >= 0LL) && (7LL - (long long )len) - (long long )position
        >= 0LL) && (2147483650LL - (long long )k) - (long long )position >= 0LL) &&
        (2147483651LL - (long long )k) - (long long )len >= 0LL) && (((int )k == 1
        || (int )k == 2) || (int )k == 3)) && (((position == 0 || position == 1) ||
        position == 2) || position == 3))) || (((((((((((((((((-4LL + (long long )k)
        + (long long )len >= 0LL && (-4LL + (long long )i) + (long long )len >= 0LL)
        && (-3LL + (long long )len) + (long long )position >= 0LL) && (-2LL - (long
        long )i) + (long long )len >= 0LL) && (3LL - (long long )len) + (long long
        )position >= 0LL) && (2147483644LL - (long long )k) + (long long )len >= 0LL)
        && (1LL + (long long )k) - (long long )position >= 0LL) && (1LL + (long long
        )i) - (long long )position >= 0LL) && (2LL + (long long )k) - (long long )len
        >= 0LL) && (2LL + (long long )i) - (long long )len >= 0LL) && (3LL - (long
        long )i) - (long long )position >= 0LL) && (4LL - (long long )i) - (long long
        )len >= 0LL) && (5LL - (long long )len) - (long long )position >= 0LL) &&
        (2147483649LL - (long long )k) - (long long )position >= 0LL) && (2147483650LL
        - (long long )k) - (long long )len >= 0LL) && ((int )k == 1 || (int )k ==
        2)) && ((position == 0 || position == 1) || position == 2))) || (((((((((((((((((-3LL
        + (long long )k) + (long long )len >= 0LL && (-3LL + (long long )i) + (long
        long )len >= 0LL) && (-2LL + (long long )len) + (long long )position >= 0LL)
        && (-1LL - (long long )i) + (long long )len >= 0LL) && (2LL - (long long )len)
        + (long long )position >= 0LL) && (2147483645LL - (long long )k) + (long long
        )len >= 0LL) && (1LL + (long long )k) - (long long )len >= 0LL) && (1LL +
        (long long )i) - (long long )len >= 0LL) && (2LL - (long long )i) - (long
        long )position >= 0LL) && (3LL - (long long )len) - (long long )position >=
        0LL) && (3LL - (long long )i) - (long long )len >= 0LL) && (2147483648LL -
        (long long )k) - (long long )position >= 0LL) && (2147483649LL - (long long
        )k) - (long long )len >= 0LL) && (long long )k - (long long )position >= 0LL)
        && (long long )i - (long long )position >= 0LL) && (int )k == 1) && (position
        == 0 || position == 1)))))) || (((((((((((((((2147483648LL + (long long )i)
        + (long long )k >= 0LL && (2147483648LL + (long long )i) + (long long )position
        >= 0LL) && (4294967296LL + (long long )k) + (long long )position >= 0LL) &&
        (2147483648LL - (long long )i) + (long long )k >= 0LL) && (2147483648LL -
        (long long )i) + (long long )position >= 0LL) && (4294967295LL - (long long
        )k) + (long long )position >= 0LL) && (2147483647LL + (long long )i) - (long
        long )k >= 0LL) && (2147483647LL + (long long )i) - (long long )position >=
        0LL) && (4294967295LL + (long long )k) - (long long )position >= 0LL) && (2147483647LL
        - (long long )i) - (long long )k >= 0LL) && (2147483647LL - (long long )i)
        - (long long )position >= 0LL) && (4294967294LL - (long long )k) - (long long
        )position >= 0LL) && 0 == i) && i == 0) && ((((((((((((((((-5LL + (long long
        )i) + (long long )len >= 0LL && (2147483643LL + (long long )len) + (long long
        )position >= 0LL) && (2147483643LL + (long long )k) + (long long )len >= 0LL)
        && (-5LL - (long long )i) + (long long )len >= 0LL) && (2147483642LL - (long
        long )k) + (long long )len >= 0LL) && (2147483653LL - (long long )len) + (long
        long )position >= 0LL) && (5LL + (long long )i) - (long long )len >= 0LL)
        && (2147483642LL + (long long )len) - (long long )position >= 0LL) && (2147483653LL
        + (long long )k) - (long long )len >= 0LL) && (5LL - (long long )i) - (long
        long )len >= 0LL) && (2147483652LL - (long long )len) - (long long )position
        >= 0LL) && (2147483652LL - (long long )k) - (long long )len >= 0LL) && (((((int
        )k == 0 || (int )k == 1) || (int )k == 2) || (int )k == 3) || (int )k == 4))
        || (((((((((((((-4LL + (long long )i) + (long long )len >= 0LL && (2147483644LL
        + (long long )len) + (long long )position >= 0LL) && (2147483644LL + (long
        long )k) + (long long )len >= 0LL) && (-4LL - (long long )i) + (long long
        )len >= 0LL) && (2147483643LL - (long long )k) + (long long )len >= 0LL) &&
        (2147483652LL - (long long )len) + (long long )position >= 0LL) && (4LL +
        (long long )i) - (long long )len >= 0LL) && (2147483643LL + (long long )len)
        - (long long )position >= 0LL) && (2147483652LL + (long long )k) - (long long
        )len >= 0LL) && (4LL - (long long )i) - (long long )len >= 0LL) && (2147483651LL
        - (long long )len) - (long long )position >= 0LL) && (2147483651LL - (long
        long )k) - (long long )len >= 0LL) && ((((int )k == 0 || (int )k == 1) ||
        (int )k == 2) || (int )k == 3))) || (((((((((((((-3LL + (long long )i) + (long
        long )len >= 0LL && (2147483645LL + (long long )len) + (long long )position
        >= 0LL) && (2147483645LL + (long long )k) + (long long )len >= 0LL) && (-3LL
        - (long long )i) + (long long )len >= 0LL) && (2147483644LL - (long long )k)
        + (long long )len >= 0LL) && (2147483651LL - (long long )len) + (long long
        )position >= 0LL) && (3LL + (long long )i) - (long long )len >= 0LL) && (2147483644LL
        + (long long )len) - (long long )position >= 0LL) && (2147483651LL + (long
        long )k) - (long long )len >= 0LL) && (3LL - (long long )i) - (long long )len
        >= 0LL) && (2147483650LL - (long long )len) - (long long )position >= 0LL)
        && (2147483650LL - (long long )k) - (long long )len >= 0LL) && (((int )k ==
        0 || (int )k == 1) || (int )k == 2))) || (((((((((((((-2LL + (long long )i)
        + (long long )len >= 0LL && (2147483646LL + (long long )len) + (long long
        )position >= 0LL) && (2147483646LL + (long long )k) + (long long )len >= 0LL)
        && (-2LL - (long long )i) + (long long )len >= 0LL) && (2147483645LL - (long
        long )k) + (long long )len >= 0LL) && (2147483650LL - (long long )len) + (long
        long )position >= 0LL) && (2LL + (long long )i) - (long long )len >= 0LL)
        && (2147483645LL + (long long )len) - (long long )position >= 0LL) && (2147483650LL
        + (long long )k) - (long long )len >= 0LL) && (2LL - (long long )i) - (long
        long )len >= 0LL) && (2147483649LL - (long long )len) - (long long )position
        >= 0LL) && (2147483649LL - (long long )k) - (long long )len >= 0LL) && ((int
        )k == 0 || (int )k == 1))))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_nondet_insert-2.i
        line: 631
        column: 3
        function: main
      value: (((int )len == 2 || (int )len == 3) || (int )len == 4) || (int )len ==
        5
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_nondet_insert-2.i
        line: 576
        column: 3
        function: sll_create
      value: (head == new_head && (((-1 <= len && ((len <= 0 || len <= 1) || len <=
        2)) || (0 <= len && len <= 3)) || (1 <= len && len <= 4))) || ((0 == head
        && head == 0) && (((len == 2 || len == 3) || len == 4) || len == 5))
      format: c_expression
