- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 2c42d9d0-588d-4ca1-ab56-af92ebf4db0f
    creation_time: 2025-03-22T17:10:43Z
    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/termination.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c: 2e6e06de31959e386aafc2fb45c848364ae9fea32df4ba40928c607f134f313f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(F end) )
  content:
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: e <= 127
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (127LL - (long long )e) + (long long )m >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (127LL - (long long )e) + (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (4294967295LL - (long long )m) + (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (4294967295LL - (long long )__retres4) + (long long )m >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (4294967295LL - (long long )__retres4) + (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (long long )m + (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (long long )__retres4 + (long long )m >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (long long )__retres4 + (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (127LL + (long long )__retres4) - (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (4294967295LL + (long long )m) - (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (4294967295LL + (long long )__retres4) - (long long )m >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (4294967295LL + (long long )__retres4) - (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (4294967422LL - (long long )e) - (long long )m >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (4294967422LL - (long long )e) - (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (4294967422LL - (long long )__retres4) - (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (8589934590LL - (long long )m) - (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (8589934590LL - (long long )__retres4) - (long long )m >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: (8589934590LL - (long long )__retres4) - (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 57
        column: 5
        function: base2flt
      value: ((((((((((-128 <= e && 16777216U <= m) && (128LL + (long long )e) + (long
        long )m >= 0LL) && (128LL + (long long )e) + (long long )res >= 0LL) && (128LL
        + (long long )__retres4) + (long long )e >= 0LL) && (4294967423LL - (long
        long )__retres4) + (long long )e >= 0LL) && (4294967423LL + (long long )e)
        - (long long )m >= 0LL) && (4294967423LL + (long long )e) - (long long )res
        >= 0LL) || ((((((-124 <= e && (124LL + (long long )e) + (long long )m >= 0LL)
        && (124LL + (long long )e) + (long long )res >= 0LL) && (124LL + (long long
        )__retres4) + (long long )e >= 0LL) && (4294967419LL - (long long )__retres4)
        + (long long )e >= 0LL) && (4294967419LL + (long long )e) - (long long )m
        >= 0LL) && (4294967419LL + (long long )e) - (long long )res >= 0LL)) || ((((((-125
        <= e && (125LL + (long long )e) + (long long )m >= 0LL) && (125LL + (long
        long )e) + (long long )res >= 0LL) && (125LL + (long long )__retres4) + (long
        long )e >= 0LL) && (4294967420LL - (long long )__retres4) + (long long )e
        >= 0LL) && (4294967420LL + (long long )e) - (long long )m >= 0LL) && (4294967420LL
        + (long long )e) - (long long )res >= 0LL)) || ((((((-126 <= e && (126LL +
        (long long )e) + (long long )m >= 0LL) && (126LL + (long long )e) + (long
        long )res >= 0LL) && (126LL + (long long )__retres4) + (long long )e >= 0LL)
        && (4294967421LL - (long long )__retres4) + (long long )e >= 0LL) && (4294967421LL
        + (long long )e) - (long long )m >= 0LL) && (4294967421LL + (long long )e)
        - (long long )res >= 0LL)) || ((((((-127 <= e && (127LL + (long long )e) +
        (long long )m >= 0LL) && (127LL + (long long )e) + (long long )res >= 0LL)
        && (127LL + (long long )__retres4) + (long long )e >= 0LL) && (4294967422LL
        - (long long )__retres4) + (long long )e >= 0LL) && (4294967422LL + (long
        long )e) - (long long )m >= 0LL) && (4294967422LL + (long long )e) - (long
        long )res >= 0LL)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: -128 <= e
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: m <= 16777215U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (128LL + (long long )e) + (long long )m >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (128LL + (long long )e) + (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (128LL + (long long )__retres4) + (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (4294967295LL - (long long )m) + (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (4294967295LL - (long long )__retres4) + (long long )m >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (4294967295LL - (long long )__retres4) + (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (4294967423LL - (long long )__retres4) + (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (long long )m + (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (long long )__retres4 + (long long )m >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (long long )__retres4 + (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (4294967295LL + (long long )m) - (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (4294967295LL + (long long )__retres4) - (long long )m >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (4294967295LL + (long long )__retres4) - (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (4294967423LL + (long long )e) - (long long )m >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (4294967423LL + (long long )e) - (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (8589934590LL - (long long )m) - (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (8589934590LL - (long long )__retres4) - (long long )m >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: (8589934590LL - (long long )__retres4) - (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/soft_float_1-3a.c.cil.c
        line: 37
        column: 5
        function: base2flt
      value: ((((((((((e <= 123 && (123LL - (long long )e) + (long long )m >= 0LL)
        && (123LL - (long long )e) + (long long )res >= 0LL) && (123LL + (long long
        )__retres4) - (long long )e >= 0LL) && (4294967418LL - (long long )e) - (long
        long )m >= 0LL) && (4294967418LL - (long long )e) - (long long )res >= 0LL)
        && (4294967418LL - (long long )__retres4) - (long long )e >= 0LL) && m % 16U
        == 0U) || (((((((e <= 124 && (124LL - (long long )e) + (long long )m >= 0LL)
        && (124LL - (long long )e) + (long long )res >= 0LL) && (124LL + (long long
        )__retres4) - (long long )e >= 0LL) && (4294967419LL - (long long )e) - (long
        long )m >= 0LL) && (4294967419LL - (long long )e) - (long long )res >= 0LL)
        && (4294967419LL - (long long )__retres4) - (long long )e >= 0LL) && m % 8U
        == 0U)) || (((((((e <= 125 && (125LL - (long long )e) + (long long )m >= 0LL)
        && (125LL - (long long )e) + (long long )res >= 0LL) && (125LL + (long long
        )__retres4) - (long long )e >= 0LL) && (4294967420LL - (long long )e) - (long
        long )m >= 0LL) && (4294967420LL - (long long )e) - (long long )res >= 0LL)
        && (4294967420LL - (long long )__retres4) - (long long )e >= 0LL) && m % 4U
        == 0U)) || (((((((e <= 126 && (126LL - (long long )e) + (long long )m >= 0LL)
        && (126LL - (long long )e) + (long long )res >= 0LL) && (126LL + (long long
        )__retres4) - (long long )e >= 0LL) && (4294967421LL - (long long )e) - (long
        long )m >= 0LL) && (4294967421LL - (long long )e) - (long long )res >= 0LL)
        && (4294967421LL - (long long )__retres4) - (long long )e >= 0LL) && m % 2U
        == 0U)) || (((((((1U <= m && e <= 127) && (127LL - (long long )e) + (long
        long )m >= 0LL) && (127LL - (long long )e) + (long long )res >= 0LL) && (127LL
        + (long long )__retres4) - (long long )e >= 0LL) && (4294967422LL - (long
        long )e) - (long long )m >= 0LL) && (4294967422LL - (long long )e) - (long
        long )res >= 0LL) && (4294967422LL - (long long )__retres4) - (long long )e
        >= 0LL)
      format: c_expression
