- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 8983ef98-e871-41fc-ad8e-f928c6854fa6
    creation_time: 2025-03-22T19:48:16Z
    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/product-lines/minepump_spec3_product53.cil.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c: e1c4d106eb612b91999bdca4bb49f57df1223b70f35ecd881d6daa6062cb1b0b
      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/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-5LL + (long long )cleanupTimeShifts) + (long long )systemActive >=
        0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-5LL + (long long )cleanupTimeShifts) + (long long )waterLevel >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-4LL + (long long )cleanupTimeShifts) + (long long )splverifierCounter
        >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-4LL + (long long )cleanupTimeShifts) + (long long )pumpRunning >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-4LL + (long long )cleanupTimeShifts) + (long long )methaneLevelCritical
        >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-2LL + (long long )systemActive) + (long long )waterLevel >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-1LL + (long long )splverifierCounter) + (long long )systemActive >=
        0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-1LL + (long long )splverifierCounter) + (long long )waterLevel >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-1LL + (long long )pumpRunning) + (long long )systemActive >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-1LL + (long long )pumpRunning) + (long long )waterLevel >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-1LL + (long long )methaneLevelCritical) + (long long )systemActive
        >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-1LL + (long long )methaneLevelCritical) + (long long )waterLevel >=
        0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-1LL - (long long )splverifierCounter) + (long long )systemActive >=
        0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-1LL - (long long )splverifierCounter) + (long long )waterLevel >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-1LL - (long long )pumpRunning) + (long long )waterLevel >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (0LL - (long long )systemActive) + (long long )waterLevel >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (3LL - (long long )cleanupTimeShifts) + (long long )systemActive >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (3LL - (long long )cleanupTimeShifts) + (long long )waterLevel >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (4LL - (long long )cleanupTimeShifts) + (long long )splverifierCounter
        >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (4LL - (long long )cleanupTimeShifts) + (long long )pumpRunning >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (4LL - (long long )cleanupTimeShifts) + (long long )methaneLevelCritical
        >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (long long )pumpRunning + (long long )splverifierCounter >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (long long )methaneLevelCritical + (long long )splverifierCounter >=
        0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (long long )methaneLevelCritical + (long long )pumpRunning >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-4LL + (long long )cleanupTimeShifts) - (long long )splverifierCounter
        >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (-3LL + (long long )cleanupTimeShifts) - (long long )systemActive >=
        0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (1LL + (long long )splverifierCounter) - (long long )systemActive >=
        0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (1LL + (long long )pumpRunning) - (long long )systemActive >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (1LL + (long long )pumpRunning) - (long long )waterLevel >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (1LL + (long long )methaneLevelCritical) - (long long )systemActive >=
        0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (1LL - (long long )splverifierCounter) - (long long )systemActive >=
        0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (4LL - (long long )cleanupTimeShifts) - (long long )splverifierCounter
        >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (5LL - (long long )cleanupTimeShifts) - (long long )systemActive >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (long long )pumpRunning - (long long )splverifierCounter >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (long long )methaneLevelCritical - (long long )splverifierCounter >=
        0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: splverifierCounter == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: systemActive == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: cleanupTimeShifts == 4
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/minepump_spec3_product53.cil.c
        line: 111
        column: 3
        function: test
      value: (((((((((((((((((((((((((((((0LL - (long long )pumpRunning) + (long long
        )systemActive >= 0LL && (0LL - (long long )methaneLevelCritical) + (long long
        )systemActive >= 0LL) && (0LL - (long long )methaneLevelCritical) + (long
        long )waterLevel >= 0LL) && (1LL - (long long )pumpRunning) + (long long )splverifierCounter
        >= 0LL) && (1LL - (long long )methaneLevelCritical) + (long long )splverifierCounter
        >= 0LL) && (1LL - (long long )methaneLevelCritical) + (long long )pumpRunning
        >= 0LL) && (-3LL + (long long )cleanupTimeShifts) - (long long )pumpRunning
        >= 0LL) && (-3LL + (long long )cleanupTimeShifts) - (long long )methaneLevelCritical
        >= 0LL) && (-2LL + (long long )cleanupTimeShifts) - (long long )waterLevel
        >= 0LL) && (1LL + (long long )systemActive) - (long long )waterLevel >= 0LL)
        && (1LL + (long long )methaneLevelCritical) - (long long )pumpRunning >= 0LL)
        && (2LL + (long long )splverifierCounter) - (long long )waterLevel >= 0LL)
        && (2LL + (long long )methaneLevelCritical) - (long long )waterLevel >= 0LL)
        && (1LL - (long long )pumpRunning) - (long long )splverifierCounter >= 0LL)
        && (1LL - (long long )methaneLevelCritical) - (long long )splverifierCounter
        >= 0LL) && (2LL - (long long )splverifierCounter) - (long long )waterLevel
        >= 0LL) && (2LL - (long long )pumpRunning) - (long long )systemActive >= 0LL)
        && (2LL - (long long )methaneLevelCritical) - (long long )pumpRunning >= 0LL)
        && (2LL - (long long )methaneLevelCritical) - (long long )systemActive >=
        0LL) && (3LL - (long long )pumpRunning) - (long long )waterLevel >= 0LL) &&
        (3LL - (long long )systemActive) - (long long )waterLevel >= 0LL) && (3LL
        - (long long )methaneLevelCritical) - (long long )waterLevel >= 0LL) && (5LL
        - (long long )cleanupTimeShifts) - (long long )pumpRunning >= 0LL) && (5LL
        - (long long )cleanupTimeShifts) - (long long )methaneLevelCritical >= 0LL)
        && (6LL - (long long )cleanupTimeShifts) - (long long )waterLevel >= 0LL)
        && (pumpRunning == 0 || pumpRunning == 1)) && (waterLevel == 1 || waterLevel
        == 2)) && (methaneLevelCritical == 0 || methaneLevelCritical == 1)) || (((((((((((((((((((((((((((((-1LL
        - (long long )pumpRunning) + (long long )systemActive >= 0LL && (-1LL - (long
        long )methaneLevelCritical) + (long long )systemActive >= 0LL) && (-1LL -
        (long long )methaneLevelCritical) + (long long )waterLevel >= 0LL) && (0LL
        - (long long )pumpRunning) + (long long )splverifierCounter >= 0LL) && (0LL
        - (long long )methaneLevelCritical) + (long long )splverifierCounter >= 0LL)
        && (0LL - (long long )methaneLevelCritical) + (long long )pumpRunning >= 0LL)
        && (-4LL + (long long )cleanupTimeShifts) - (long long )pumpRunning >= 0LL)
        && (-4LL + (long long )cleanupTimeShifts) - (long long )methaneLevelCritical
        >= 0LL) && (-3LL + (long long )cleanupTimeShifts) - (long long )waterLevel
        >= 0LL) && (1LL + (long long )splverifierCounter) - (long long )waterLevel
        >= 0LL) && (1LL + (long long )methaneLevelCritical) - (long long )waterLevel
        >= 0LL) && (0LL - (long long )pumpRunning) - (long long )splverifierCounter
        >= 0LL) && (0LL - (long long )methaneLevelCritical) - (long long )splverifierCounter
        >= 0LL) && (0LL - (long long )methaneLevelCritical) - (long long )pumpRunning
        >= 0LL) && (1LL - (long long )splverifierCounter) - (long long )waterLevel
        >= 0LL) && (1LL - (long long )pumpRunning) - (long long )systemActive >= 0LL)
        && (1LL - (long long )pumpRunning) - (long long )waterLevel >= 0LL) && (1LL
        - (long long )methaneLevelCritical) - (long long )systemActive >= 0LL) &&
        (1LL - (long long )methaneLevelCritical) - (long long )waterLevel >= 0LL)
        && (2LL - (long long )systemActive) - (long long )waterLevel >= 0LL) && (4LL
        - (long long )cleanupTimeShifts) - (long long )pumpRunning >= 0LL) && (4LL
        - (long long )cleanupTimeShifts) - (long long )methaneLevelCritical >= 0LL)
        && (5LL - (long long )cleanupTimeShifts) - (long long )waterLevel >= 0LL)
        && (long long )systemActive - (long long )waterLevel >= 0LL) && (long long
        )methaneLevelCritical - (long long )pumpRunning >= 0LL) && 0 == splverifierCounter)
        && pumpRunning == 0) && waterLevel == 1) && methaneLevelCritical == 0)) ||
        ((((((((((((((((((((((((((((0LL - (long long )pumpRunning) + (long long )systemActive
        >= 0LL && (0LL - (long long )methaneLevelCritical) + (long long )systemActive
        >= 0LL) && (0LL - (long long )methaneLevelCritical) + (long long )waterLevel
        >= 0LL) && (1LL - (long long )pumpRunning) + (long long )splverifierCounter
        >= 0LL) && (1LL - (long long )methaneLevelCritical) + (long long )splverifierCounter
        >= 0LL) && (1LL - (long long )methaneLevelCritical) + (long long )pumpRunning
        >= 0LL) && (-3LL + (long long )cleanupTimeShifts) - (long long )pumpRunning
        >= 0LL) && (-3LL + (long long )cleanupTimeShifts) - (long long )methaneLevelCritical
        >= 0LL) && (-2LL + (long long )cleanupTimeShifts) - (long long )waterLevel
        >= 0LL) && (1LL + (long long )systemActive) - (long long )waterLevel >= 0LL)
        && (1LL + (long long )methaneLevelCritical) - (long long )pumpRunning >= 0LL)
        && (2LL + (long long )splverifierCounter) - (long long )waterLevel >= 0LL)
        && (2LL + (long long )methaneLevelCritical) - (long long )waterLevel >= 0LL)
        && (1LL - (long long )pumpRunning) - (long long )splverifierCounter >= 0LL)
        && (1LL - (long long )methaneLevelCritical) - (long long )splverifierCounter
        >= 0LL) && (2LL - (long long )splverifierCounter) - (long long )waterLevel
        >= 0LL) && (2LL - (long long )pumpRunning) - (long long )systemActive >= 0LL)
        && (2LL - (long long )methaneLevelCritical) - (long long )pumpRunning >= 0LL)
        && (2LL - (long long )methaneLevelCritical) - (long long )systemActive >=
        0LL) && (3LL - (long long )pumpRunning) - (long long )waterLevel >= 0LL) &&
        (3LL - (long long )systemActive) - (long long )waterLevel >= 0LL) && (3LL
        - (long long )methaneLevelCritical) - (long long )waterLevel >= 0LL) && (5LL
        - (long long )cleanupTimeShifts) - (long long )pumpRunning >= 0LL) && (5LL
        - (long long )cleanupTimeShifts) - (long long )methaneLevelCritical >= 0LL)
        && (6LL - (long long )cleanupTimeShifts) - (long long )waterLevel >= 0LL)
        && (pumpRunning == 0 || pumpRunning == 1)) && (waterLevel == 1 || waterLevel
        == 2)) && (methaneLevelCritical == 0 || methaneLevelCritical == 1))
      format: c_expression
