- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 17105530-4d2e-4631-9e6e-f52ddc043711
    creation_time: 2025-03-22T17:10:52Z
    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/openssl-simplified/s3_srvr_1b.cil.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl-simplified/s3_srvr_1b.cil.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl-simplified/s3_srvr_1b.cil.c: 153b6d90c91de27e09ed3c918b0b1be779b258e790f6fc392e7d5f390719c2db
      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/openssl-simplified/s3_srvr_1b.cil.c
        line: 29
        column: 3
        function: main
      value: (((8654LL + (long long )blastFlag) - (long long )s__state >= 0LL && (((((((((((((((-8468LL
        + (long long )blastFlag) + (long long )s__state >= 0LL && (2147475038LL +
        (long long )s__hit) + (long long )s__state >= 0LL) && (2147483501LL + (long
        long )blastFlag) + (long long )s__hit >= 0LL) && (-8461LL - (long long )blastFlag)
        + (long long )s__state >= 0LL) && (2147475037LL - (long long )s__hit) + (long
        long )s__state >= 0LL) && (2147483509LL - (long long )blastFlag) + (long long
        )s__hit >= 0LL) && (2147483500LL + (long long )blastFlag) - (long long )s__hit
        >= 0LL) && (2147492159LL + (long long )s__hit) - (long long )s__state >= 0LL)
        && (8661LL - (long long )blastFlag) - (long long )s__state >= 0LL) && (2147483508LL
        - (long long )blastFlag) - (long long )s__hit >= 0LL) && (2147492158LL - (long
        long )s__hit) - (long long )s__state >= 0LL) && (((s__state == 8466 || s__state
        == 8512) || s__state == 8640) || s__state == 8656)) && (((blastFlag == 2 ||
        blastFlag == 3) || blastFlag == 4) || blastFlag == 5)) || ((((((((((((((-8514LL
        + (long long )blastFlag) + (long long )s__state >= 0LL && (2147474992LL +
        (long long )s__hit) + (long long )s__state >= 0LL) && (2147483646LL + (long
        long )blastFlag) + (long long )s__hit >= 0LL) && (-8510LL - (long long )blastFlag)
        + (long long )s__state >= 0LL) && (2147474991LL - (long long )s__hit) + (long
        long )s__state >= 0LL) && (2147483650LL - (long long )blastFlag) + (long long
        )s__hit >= 0LL) && (2147483645LL + (long long )blastFlag) - (long long )s__hit
        >= 0LL) && (2147492304LL + (long long )s__hit) - (long long )s__state >= 0LL)
        && (8658LL - (long long )blastFlag) - (long long )s__state >= 0LL) && (2147483649LL
        - (long long )blastFlag) - (long long )s__hit >= 0LL) && (2147492303LL - (long
        long )s__hit) - (long long )s__state >= 0LL) && 2 == blastFlag) && blastFlag
        == 2) && (s__state == 8512 || s__state == 8656))) || (((((((((((((-8514LL
        + (long long )blastFlag) + (long long )s__state >= 0LL && (2147474848LL +
        (long long )s__hit) + (long long )s__state >= 0LL) && (2147483502LL + (long
        long )blastFlag) + (long long )s__hit >= 0LL) && (-8510LL - (long long )blastFlag)
        + (long long )s__state >= 0LL) && (2147474847LL - (long long )s__hit) + (long
        long )s__state >= 0LL) && (2147483506LL - (long long )blastFlag) + (long long
        )s__hit >= 0LL) && (2147483501LL + (long long )blastFlag) - (long long )s__hit
        >= 0LL) && (2147492160LL + (long long )s__hit) - (long long )s__state >= 0LL)
        && (8660LL - (long long )blastFlag) - (long long )s__state >= 0LL) && (2147483505LL
        - (long long )blastFlag) - (long long )s__hit >= 0LL) && (2147492159LL - (long
        long )s__hit) - (long long )s__state >= 0LL) && (s__state == 8512 || s__state
        == 8656)) && (blastFlag == 2 || blastFlag == 4)))) || ((((((((((((((((-8466LL
        + (long long )blastFlag) + (long long )s__state >= 0LL && (2147475182LL +
        (long long )s__hit) + (long long )s__state >= 0LL) && (2147483648LL + (long
        long )blastFlag) + (long long )s__hit >= 0LL) && (-8466LL - (long long )blastFlag)
        + (long long )s__state >= 0LL) && (2147475181LL - (long long )s__hit) + (long
        long )s__state >= 0LL) && (2147483648LL - (long long )blastFlag) + (long long
        )s__hit >= 0LL) && (8466LL + (long long )blastFlag) - (long long )s__state
        >= 0LL) && (2147483647LL + (long long )blastFlag) - (long long )s__hit >=
        0LL) && (2147492114LL + (long long )s__hit) - (long long )s__state >= 0LL)
        && (8466LL - (long long )blastFlag) - (long long )s__state >= 0LL) && (2147483647LL
        - (long long )blastFlag) - (long long )s__hit >= 0LL) && (2147492113LL - (long
        long )s__hit) - (long long )s__state >= 0LL) && 0 == blastFlag) && 8466 ==
        s__state) && s__state == 8466) && blastFlag == 0)) || ((((((((((((((-8468LL
        + (long long )blastFlag) + (long long )s__state >= 0LL && (2147475038LL +
        (long long )s__hit) + (long long )s__state >= 0LL) && (2147483645LL + (long
        long )blastFlag) + (long long )s__hit >= 0LL) && (-8464LL - (long long )blastFlag)
        + (long long )s__state >= 0LL) && (2147475037LL - (long long )s__hit) + (long
        long )s__state >= 0LL) && (2147483651LL - (long long )blastFlag) + (long long
        )s__hit >= 0LL) && (8638LL + (long long )blastFlag) - (long long )s__state
        >= 0LL) && (2147483644LL + (long long )blastFlag) - (long long )s__hit >=
        0LL) && (2147492288LL + (long long )s__hit) - (long long )s__state >= 0LL)
        && (8643LL - (long long )blastFlag) - (long long )s__state >= 0LL) && (2147483650LL
        - (long long )blastFlag) - (long long )s__hit >= 0LL) && (2147492287LL - (long
        long )s__hit) - (long long )s__state >= 0LL) && (s__state == 8466 || s__state
        == 8640)) && (blastFlag == 2 || blastFlag == 3))
      format: c_expression
