{ "spark": [ { "name": "RFLX.RFLX_Types", "sloc": [ { "file": "rflx-rflx_types.ads", "line": 6 } ], "spark": "all" }, { "name": "RFLX.RFLX_Types.Byte_Index", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 35 }, { "file": "rflx-rflx_types.ads", "line": 6 } ], "spark": "all" }, { "name": "RFLX.RFLX_Types.First_Bit_Index", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 38 }, { "file": "rflx-rflx_types.ads", "line": 6 } ], "spark": "all" }, { "name": "RFLX.RFLX_Types.Last_Bit_Index", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 41 }, { "file": "rflx-rflx_types.ads", "line": 6 } ], "spark": "all" }, { "name": "RFLX.RFLX_Types.Unreachable_Bit_Length", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 65 }, { "file": "rflx-rflx_types.ads", "line": 6 } ], "spark": "all" }, { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ], "spark": "all" }, { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ], "spark": "all" }, { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ], "spark": "all" }, { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ], "spark": "all" }, { "name": "RFLX.RFLX_Types.U64_Extract.D.ES", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 115 }, { "file": "rflx-rflx_types.ads", "line": 6 } ], "spark": "all" }, { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ], "spark": "all" }, { "name": "RFLX.RFLX_Types.U64_Insert.Read", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 184 }, { "file": "rflx-rflx_types.ads", "line": 6 } ], "spark": "all" }, { "name": "RFLX.RFLX_Types.U64_Insert.Write", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 192 }, { "file": "rflx-rflx_types.ads", "line": 6 } ], "spark": "all" } ], "flow": [ { "file": "rflx-rflx_generic_types.adb", "line": 200, "col": 7, "rule": "UNINITIALIZED", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": { }, "msg_id": 0, "how_proved": "flow" } ], "session_map": { " 1": "/home/tr/sync/RecordFlux/build/gnatprove/ada___rflx__rflx_types__byte_index", " 2": "/home/tr/sync/RecordFlux/build/gnatprove/ada___rflx__rflx_types__unreachable_bit_length", " 3": "/home/tr/sync/RecordFlux/build/gnatprove/ada___rflx__rflx_types__u64_extract__d__es", " 4": "/home/tr/sync/RecordFlux/build/gnatprove/ada___rflx__rflx_types__u64_insert__write", " 5": "/home/tr/sync/RecordFlux/build/gnatprove/ada___rflx__rflx_types__u64_insert__read", " 6": "/home/tr/sync/RecordFlux/build/gnatprove/ada___rflx__rflx_types__u64_extract__d", " 7": "/home/tr/sync/RecordFlux/build/gnatprove/ada___rflx__rflx_types__u64_extract_intermediate", " 8": "/home/tr/sync/RecordFlux/build/gnatprove/ada___rflx__rflx_types__u64_extract_remaining", " 9": "/home/tr/sync/RecordFlux/build/gnatprove/ada___rflx__rflx_types__u64_extract", " 10": "/home/tr/sync/RecordFlux/build/gnatprove/ada___rflx__rflx_types__u64_insert" }, "proof": [ { "file": "rflx-rflx_generic_types.ads", "line": 36, "col": 36, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.Byte_Index", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 35 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 821, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.ads", "check_line": 36, "check_col": 36, "msg_id": 1, "session_dir": 1, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.ads", "line": 36, "col": 36, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.Byte_Index", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 35 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 8926, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.ads", "check_line": 36, "check_col": 36, "msg_id": 2, "session_dir": 1, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.ads", "line": 36, "col": 41, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.Byte_Index", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 35 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 9016, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.ads", "check_line": 36, "check_col": 41, "msg_id": 3, "session_dir": 1, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.ads", "line": 69, "col": 10, "rule": "VC_INCONSISTENT_PRE", "severity": "warning", "entity": { "name": "RFLX.RFLX_Types.Unreachable_Bit_Length", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 65 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.ads", "check_line": 69, "check_col": 10, "msg_id": 4, "session_dir": 2, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 115, "col": 65, "rule": "VC_POSTCONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D.ES", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 115 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 14, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 115, "check_col": 65, "msg_id": 5, "session_dir": 3, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 197, "col": 48, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert.Write", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 192 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 16548, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 197, "check_col": 48, "msg_id": 6, "session_dir": 4, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 197, "col": 48, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert.Write", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 192 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 16791, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 197, "check_col": 48, "msg_id": 7, "session_dir": 4, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 197, "col": 16, "rule": "VC_INDEX_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert.Write", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 192 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6596, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 17006, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 197, "check_col": 16, "msg_id": 8, "session_dir": 4, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 189, "col": 55, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert.Read", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 184 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 16501, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 189, "check_col": 55, "msg_id": 9, "session_dir": 5, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 189, "col": 55, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert.Read", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 184 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 16744, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 189, "check_col": 55, "msg_id": 10, "session_dir": 5, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 189, "col": 23, "rule": "VC_INDEX_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert.Read", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 184 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6549, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 16959, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 189, "check_col": 23, "msg_id": 11, "session_dir": 5, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 116, "col": 46, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 36011, "time": 3.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 116, "check_col": 46, "msg_id": 12, "session_dir": 6, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 2.99999993294477E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 116, "col": 59, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 35631, "time": 3.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 116, "check_col": 59, "msg_id": 13, "session_dir": 6, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 2.99999993294477E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 116, "col": 76, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4390, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 116, "check_col": 76, "msg_id": 14, "session_dir": 6, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 116, "col": 83, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4436, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 116, "check_col": 83, "msg_id": 15, "session_dir": 6, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 116, "col": 83, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4461, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 116, "check_col": 83, "msg_id": 16, "session_dir": 6, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 117, "col": 41, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 12361, "time": 2.11000000000000E+00 }, "Z3": { "result": "Out Of Memory", "steps": -1, "time": 9.25000000000000E+00 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 117, "check_col": 41, "msg_id": 17, "session_dir": 6, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 1, "max_time": 2.10999989509583E+00 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 117, "col": 25, "rule": "VC_ASSERT", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 25745, "time": 4.68000000000000E+00 }, "Z3": { "result": "Out Of Memory", "steps": -1, "time": 9.51000000000000E+00 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 117, "check_col": 25, "msg_id": 18, "session_dir": 6, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 308, "max_time": 4.67999982833862E+00 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 123, "col": 34, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 681, "time": 5.00000000000000E-02 }, "Z3": { "result": "Out Of Memory", "steps": -1, "time": 8.97000000000000E+00 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 123, "check_col": 34, "msg_id": 19, "session_dir": 6, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 123, "col": 45, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 38748, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 123, "check_col": 45, "msg_id": 20, "session_dir": 6, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 123, "col": 45, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 965, "time": 7.00000000000000E-02 }, "Z3": { "result": "Out Of Memory", "steps": -1, "time": 9 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 123, "check_col": 45, "msg_id": 21, "session_dir": 6, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 1, "max_time": 7.00000002980232E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 120, "col": 66, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5701, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 120, "check_col": 66, "msg_id": 22, "session_dir": 6, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 120, "col": 66, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5734, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 120, "check_col": 66, "msg_id": 23, "session_dir": 6, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 120, "col": 77, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 841, "time": 6.00000000000000E-02 }, "Z3": { "result": "Out Of Memory", "steps": -1, "time": 9.03000000000000E+00 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 120, "check_col": 77, "msg_id": 24, "session_dir": 6, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 1, "max_time": 5.99999986588955E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 120, "col": 77, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 37189, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 120, "check_col": 77, "msg_id": 25, "session_dir": 6, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 121, "col": 75, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 61787, "time": 3.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 121, "check_col": 75, "msg_id": 26, "session_dir": 6, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 2.99999993294477E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 121, "col": 75, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 72, "time": 4.00000000000000E-02 }, "Z3": { "result": "Out Of Memory", "steps": -1, "time": 8.61000000000000E+00 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 121, "check_col": 75, "msg_id": 27, "session_dir": 6, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 121, "col": 43, "rule": "VC_INDEX_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 17767, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 72, "time": 4.00000000000000E-02 }, "Z3": { "result": "Out Of Memory", "steps": -1, "time": 8.97000000000000E+00 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 121, "check_col": 43, "msg_id": 28, "session_dir": 6, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 1, "max_time": 3.99999991059303E-02 }, "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 121, "col": 37, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3694, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 121, "check_col": 37, "msg_id": 29, "session_dir": 6, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 60, "col": 33, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { }, "transformations": { "trivial_true": [ ] } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 1289, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 12723, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5333, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5321, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 12669, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 1252, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 60, "check_col": 33, "msg_id": 30, "session_dir": 7, "how_proved": "prover", "stats": { "Trivial": { "count": 1, "max_steps": 0, "max_time": 0.00000000000000E+00 }, "Z3": { "count": 6, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 62, "col": 61, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 179947, "time": 3.04000000000000E+00 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 62, "check_col": 61, "msg_id": 31, "session_dir": 7, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 4713, "max_time": 3.03999996185303E+00 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 62, "col": 86, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 14011, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 62, "check_col": 86, "msg_id": 32, "session_dir": 7, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 62, "col": 39, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { }, "transformations": { "trivial_true": [ ] } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 206823, "time": 6.69000000000000E+00 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4001, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4001, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 14124, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 14168, "time": 3.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 62, "check_col": 39, "msg_id": 33, "session_dir": 7, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 5481, "max_time": 6.69000005722046E+00 }, "Trivial": { "count": 1, "max_steps": 0, "max_time": 0.00000000000000E+00 }, "Z3": { "count": 4, "max_steps": 1, "max_time": 2.99999993294477E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 63, "col": 49, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 742, "time": 4.00000000000000E-02 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 63, "check_col": 49, "msg_id": 34, "session_dir": 7, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 65, "col": 34, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 8989120, "time": 2.67000000000000E+00 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 65, "check_col": 34, "msg_id": 35, "session_dir": 7, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 10674, "max_time": 2.67000007629395E+00 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 65, "col": 14, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { }, "transformations": { "trivial_true": [ ] } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 3051, "time": 1.46000000000000E+00 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 1540, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 15609, "time": 2.80000000000000E-01 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 15567, "time": 2.60000000000000E-01 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 1536, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 65, "check_col": 14, "msg_id": 36, "session_dir": 7, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 1, "max_time": 1.46000003814697E+00 }, "Trivial": { "count": 1, "max_steps": 0, "max_time": 0.00000000000000E+00 }, "Z3": { "count": 4, "max_steps": 1, "max_time": 2.80000001192093E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 57, "col": 69, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2328, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2210, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 57, "check_col": 69, "msg_id": 37, "session_dir": 7, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 57, "col": 85, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 155180, "time": 3.60000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 57, "check_col": 85, "msg_id": 38, "session_dir": 7, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 3.60000014305115E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 58, "col": 58, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 32665, "time": 3.30000000000000E-01 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 32499, "time": 3.20000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 58, "check_col": 58, "msg_id": 39, "session_dir": 7, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 3.30000013113022E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 58, "col": 82, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 2082, "time": 1.32000000000000E+00 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 58, "check_col": 82, "msg_id": 40, "session_dir": 7, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 1, "max_time": 1.32000005245209E+00 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 56, "col": 22, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 20213, "time": 2.70000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 56, "check_col": 22, "msg_id": 41, "session_dir": 7, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 2.70000010728836E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 54, "col": 26, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 12948, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 54, "check_col": 26, "msg_id": 42, "session_dir": 7, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 56, "col": 9, "rule": "VC_POSTCONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6663, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6846, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 56, "check_col": 9, "msg_id": 43, "session_dir": 7, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 87, "col": 58, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 78886, "time": 1.24000000000000E+00 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 87, "check_col": 58, "msg_id": 44, "session_dir": 8, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 1826, "max_time": 1.24000000953674E+00 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 87, "col": 81, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 12034, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 87, "check_col": 81, "msg_id": 45, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 87, "col": 40, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { }, "transformations": { "trivial_true": [ ] } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 196625, "time": 3.46000000000000E+00 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 11857, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 11857, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 11853, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 11813, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 11849, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 87, "check_col": 40, "msg_id": 46, "session_dir": 8, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 5190, "max_time": 3.46000003814697E+00 }, "Trivial": { "count": 1, "max_steps": 0, "max_time": 0.00000000000000E+00 }, "Z3": { "count": 5, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 89, "col": 51, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13764, "time": 8.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 89, "check_col": 51, "msg_id": 47, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 7.99999982118607E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 89, "col": 51, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 1789, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 89, "check_col": 51, "msg_id": 48, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 89, "col": 75, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13565, "time": 9.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 89, "check_col": 75, "msg_id": 49, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.00000035762787E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 89, "col": 14, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { }, "transformations": { "trivial_true": [ ] } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5599, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13796, "time": 8.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13789, "time": 9.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13600, "time": 8.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13648, "time": 9.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 89, "check_col": 14, "msg_id": 50, "session_dir": 8, "how_proved": "prover", "stats": { "Trivial": { "count": 1, "max_steps": 0, "max_time": 0.00000000000000E+00 }, "Z3": { "count": 5, "max_steps": 1, "max_time": 9.00000035762787E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 81, "col": 62, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2373, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2202, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 81, "check_col": 62, "msg_id": 51, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 81, "col": 88, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2362, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2191, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 81, "check_col": 88, "msg_id": 52, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 81, "col": 75, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2360, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2189, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 81, "check_col": 75, "msg_id": 53, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 81, "col": 75, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2373, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2202, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 81, "check_col": 75, "msg_id": 54, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 82, "col": 65, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2320, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2278, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 82, "check_col": 65, "msg_id": 55, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 82, "col": 43, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 157435, "time": 2.00000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 82, "check_col": 43, "msg_id": 56, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 2.00000002980232E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 83, "col": 34, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2101, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 83, "check_col": 34, "msg_id": 57, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 83, "col": 60, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2090, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 83, "check_col": 60, "msg_id": 58, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 83, "col": 47, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2084, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 83, "check_col": 47, "msg_id": 59, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 83, "col": 47, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 15706, "time": 1.00000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 83, "check_col": 47, "msg_id": 60, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.00000001490116E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 83, "col": 101, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2042, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 83, "check_col": 101, "msg_id": 61, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 85, "col": 74, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2176, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2134, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2092, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 2044, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 85, "check_col": 74, "msg_id": 62, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 4, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 85, "col": 52, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 38747, "time": 1.20000000000000E-01 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 38551, "time": 1.20000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 85, "check_col": 52, "msg_id": 63, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.19999997317791E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 85, "col": 91, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 910628, "time": 1.01200000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 85, "check_col": 91, "msg_id": 64, "session_dir": 8, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 25590, "max_time": 1.01199998855591E+01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 79, "col": 20, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 1987, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 79, "check_col": 20, "msg_id": 65, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 79, "col": 46, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 1976, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 79, "check_col": 46, "msg_id": 66, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 79, "col": 33, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 15332, "time": 1.10000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 79, "check_col": 33, "msg_id": 67, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.09999999403954E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 75, "col": 21, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 11440, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 75, "check_col": 21, "msg_id": 68, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 78, "col": 9, "rule": "VC_POSTCONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6432, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 1979, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6631, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 78, "check_col": 9, "msg_id": 69, "session_dir": 8, "how_proved": "prover", "stats": { "Z3": { "count": 3, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 103, "col": 64, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3346, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 103, "check_col": 64, "msg_id": 70, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 104, "col": 73, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 35107, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 104, "check_col": 73, "msg_id": 71, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 104, "col": 91, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3411, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 104, "check_col": 91, "msg_id": 72, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 106, "col": 64, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3445, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 106, "check_col": 64, "msg_id": 73, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 107, "col": 50, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 9289, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 107, "check_col": 50, "msg_id": 74, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 109, "col": 52, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 34859, "time": 3.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 109, "check_col": 52, "msg_id": 75, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 2.99999993294477E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 109, "col": 65, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 34340, "time": 3.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 109, "check_col": 65, "msg_id": 76, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 2.99999993294477E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 109, "col": 82, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3586, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 109, "check_col": 82, "msg_id": 77, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 109, "col": 96, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3608, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 109, "check_col": 96, "msg_id": 78, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 131, "col": 65, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4668, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4664, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 49625, "time": 4.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 217200, "time": 1.80000000000000E-01 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4427, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4423, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 48111, "time": 3.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 128342, "time": 6.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4073, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4069, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 45255, "time": 3.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 104029, "time": 5.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3832, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3828, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 35202, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 38360, "time": 3.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 131, "check_col": 65, "msg_id": 79, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 16, "max_steps": 1, "max_time": 1.80000007152557E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 131, "col": 59, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6120, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 263445, "time": 1.30000000000000E-01 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5255, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 47928, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 131, "check_col": 59, "msg_id": 80, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 4, "max_steps": 1, "max_time": 1.29999995231628E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 132, "col": 70, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6082, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 50177, "time": 4.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5225, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 35380, "time": 3.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 132, "check_col": 70, "msg_id": 81, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 4, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 132, "col": 65, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4649, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4645, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 49610, "time": 4.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 216496, "time": 1.70000000000000E-01 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4400, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4396, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 47809, "time": 3.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 127425, "time": 6.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4054, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4050, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 45237, "time": 3.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 102805, "time": 6.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3805, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3801, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 34838, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 37684, "time": 3.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 132, "check_col": 65, "msg_id": 82, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 16, "max_steps": 1, "max_time": 1.70000001788139E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 132, "col": 59, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6101, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 193988, "time": 9.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5240, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 43983, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 132, "check_col": 59, "msg_id": 83, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 4, "max_steps": 1, "max_time": 9.00000035762787E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 135, "col": 78, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6031, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 48091, "time": 4.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5190, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 10008, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 135, "check_col": 78, "msg_id": 84, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 4, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 135, "col": 78, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6048, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 48278, "time": 3.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5203, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 10081, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 135, "check_col": 78, "msg_id": 85, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 4, "max_steps": 1, "max_time": 2.99999993294477E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 135, "col": 65, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6065, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 48522, "time": 4.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5212, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 10216, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 135, "check_col": 65, "msg_id": 86, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 4, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 131, "col": 29, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13295, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 72381, "time": 5.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13275, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4685, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 15523, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4685, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 2636744, "time": 3.34700000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 3483618, "time": 2.33900000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 12600, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 52923, "time": 3.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 12580, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4452, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 14771, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4452, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 2217881, "time": 1.48200000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 1092361, "time": 1.31500000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 11171, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 11165, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 11153, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4090, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13179, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4090, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 1655746, "time": 3.79300000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 2432646, "time": 1.66300000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 10482, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 10476, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 10464, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3857, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 12461, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3857, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 1602776, "time": 1.08600000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 467184, "time": 4.28000000000000E+00 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 131, "check_col": 29, "msg_id": 87, "session_dir": 9, "how_proved": "prover", "stats": { "CVC4": { "count": 8, "max_steps": 99104, "max_time": 3.79300003051758E+01 }, "Z3": { "count": 24, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 131, "col": 27, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 1240724, "time": 2.70600000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5232, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 131, "check_col": 27, "msg_id": 88, "session_dir": 9, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 35021, "max_time": 2.70599994659424E+01 }, "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 139, "col": 86, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6302, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5471, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 139, "check_col": 86, "msg_id": 89, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 139, "col": 86, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6319, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5488, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 139, "check_col": 86, "msg_id": 90, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 139, "col": 73, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6336, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5505, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 139, "check_col": 73, "msg_id": 91, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 139, "col": 61, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 51540, "time": 4.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 11807, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 139, "check_col": 61, "msg_id": 92, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 137, "col": 63, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6218, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5387, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 137, "check_col": 63, "msg_id": 93, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 137, "col": 58, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 50949, "time": 4.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 11529, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 137, "check_col": 58, "msg_id": 94, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 137, "col": 46, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 51146, "time": 4.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 11614, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 137, "check_col": 46, "msg_id": 95, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 137, "col": 33, "rule": "VC_LOOP_INVARIANT_INIT", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 47021, "time": 3.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4175, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 137, "check_col": 33, "msg_id": 96, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 2.99999993294477E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 137, "col": 33, "rule": "VC_LOOP_INVARIANT_PRESERV", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 1410144, "time": 2.50200000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4770, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 137, "check_col": 33, "msg_id": 97, "session_dir": 9, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 39862, "max_time": 2.50200004577637E+01 }, "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 136, "col": 35, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6201, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5370, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 136, "check_col": 35, "msg_id": 98, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 136, "col": 33, "rule": "VC_LOOP_INVARIANT_PRESERV", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 72552, "time": 5.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 136, "check_col": 33, "msg_id": 99, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 136, "col": 33, "rule": "VC_LOOP_INVARIANT_INIT", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 11414, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 136, "check_col": 33, "msg_id": 100, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 129, "col": 39, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 35336, "time": 3.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 129, "check_col": 39, "msg_id": 101, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 2.99999993294477E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 147, "col": 30, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 1259723, "time": 2.48100000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 147, "check_col": 30, "msg_id": 102, "session_dir": 9, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 35564, "max_time": 2.48099994659424E+01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 144, "col": 68, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 50838, "time": 3.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 144, "check_col": 68, "msg_id": 103, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 2.99999993294477E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 144, "col": 68, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 51182, "time": 4.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 144, "check_col": 68, "msg_id": 104, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 145, "col": 68, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4461, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4457, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 19788, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 78683, "time": 5.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 145, "check_col": 68, "msg_id": 105, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 4, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 145, "col": 62, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 169010, "time": 1.00000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 145, "check_col": 62, "msg_id": 106, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.00000001490116E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 145, "col": 35, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 602295, "time": 1.60000000000000E-01 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 41264, "time": 3.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 41216, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13995, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4482, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13995, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4482, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 145, "check_col": 35, "msg_id": 107, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 7, "max_steps": 191, "max_time": 1.59999996423721E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 151, "col": 52, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 1380321, "time": 1.95700000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 151, "check_col": 52, "msg_id": 108, "session_dir": 9, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 39010, "max_time": 1.95699996948242E+01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 97, "col": 48, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 33640, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 97, "check_col": 48, "msg_id": 109, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 97, "col": 66, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3275, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 97, "check_col": 66, "msg_id": 110, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 98, "col": 34, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5411, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 98, "check_col": 34, "msg_id": 111, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 98, "col": 52, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3372, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 98, "check_col": 52, "msg_id": 112, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 99, "col": 46, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3385, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 99, "check_col": 46, "msg_id": 113, "session_dir": 9, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 101, "col": 9, "rule": "VC_POSTCONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { }, "transformations": { "trivial_true": [ ] } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 1724694, "time": 2.33300000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 101, "check_col": 9, "msg_id": 114, "session_dir": 9, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 48849, "max_time": 2.33299999237061E+01 }, "Trivial": { "count": 1, "max_steps": 0, "max_time": 0.00000000000000E+00 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 175, "col": 64, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3483, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 175, "check_col": 64, "msg_id": 115, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 176, "col": 73, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 56549, "time": 4.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 176, "check_col": 73, "msg_id": 116, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 176, "col": 101, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3548, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 176, "check_col": 101, "msg_id": 117, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 178, "col": 64, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3582, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 178, "check_col": 64, "msg_id": 118, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 179, "col": 50, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 10024, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 179, "check_col": 50, "msg_id": 119, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 181, "col": 52, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 36029, "time": 3.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 181, "check_col": 52, "msg_id": 120, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 2.99999993294477E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 181, "col": 65, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 35354, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 181, "check_col": 65, "msg_id": 121, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 181, "col": 82, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3725, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 181, "check_col": 82, "msg_id": 122, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 181, "col": 96, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3747, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 181, "check_col": 96, "msg_id": 123, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 182, "col": 50, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 10526, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 182, "check_col": 50, "msg_id": 124, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 229, "col": 49, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 407010, "time": 1.60000000000000E-01 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 407010, "time": 1.60000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 229, "check_col": 49, "msg_id": 125, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.59999996423721E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 229, "col": 59, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 705274, "time": 2.50000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 229, "check_col": 59, "msg_id": 126, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 320, "max_time": 2.50000000000000E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 229, "col": 59, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 3321417, "time": 5.41500000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4565, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 229, "check_col": 59, "msg_id": 127, "session_dir": 10, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 94470, "max_time": 5.41500015258789E+01 }, "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 229, "col": 13, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 54528, "time": 5.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 392024, "time": 2.00000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 229, "check_col": 13, "msg_id": 128, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 2.00000002980232E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 217, "col": 44, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 36500, "time": 3.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 217, "check_col": 44, "msg_id": 129, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 2.99999993294477E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 219, "col": 59, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 36745, "time": 3.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 77794, "time": 4.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 219, "check_col": 59, "msg_id": 130, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 219, "col": 53, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 96112, "time": 5.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 219, "check_col": 53, "msg_id": 131, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 219, "col": 39, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 12134, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 219, "check_col": 39, "msg_id": 132, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 221, "col": 62, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 17908, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 98482, "time": 6.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 221, "check_col": 62, "msg_id": 133, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 5.99999986588955E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 221, "col": 56, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 101701, "time": 6.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 221, "check_col": 56, "msg_id": 134, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 5.99999986588955E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 221, "col": 99, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 22826, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 221, "check_col": 99, "msg_id": 135, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 221, "col": 39, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { }, "transformations": { "trivial_true": [ ] } }, { "proof_attempts": { "CVC4": { "result": "Timeout", "steps": -1, "time": 120 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 }, "altergo": { "result": "Valid", "steps": 3009, "time": 1.81900000000000E-01 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 46841, "time": 3.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 228208, "time": 5.16000000000000E+00 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 228208, "time": 5.12000000000000E+00 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 113604, "time": 6.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4080, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 221, "check_col": 39, "msg_id": 136, "session_dir": 10, "how_proved": "prover", "stats": { "CVC4": { "count": 2, "max_steps": 6092, "max_time": 5.15999984741211E+00 }, "Trivial": { "count": 1, "max_steps": 0, "max_time": 0.00000000000000E+00 }, "Z3": { "count": 3, "max_steps": 1, "max_time": 5.99999986588955E-02 }, "altergo": { "count": 1, "max_steps": 3010, "max_time": 1.81899994611740E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 224, "col": 59, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 18636, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 224, "check_col": 59, "msg_id": 137, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 224, "col": 39, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { }, "transformations": { "trivial_true": [ ] } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 23777, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 379425, "time": 2.10000000000000E-01 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 51825, "time": 5.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 12969, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 18573, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 224, "check_col": 39, "msg_id": 138, "session_dir": 10, "how_proved": "prover", "stats": { "Trivial": { "count": 1, "max_steps": 0, "max_time": 0.00000000000000E+00 }, "Z3": { "count": 5, "max_steps": 1, "max_time": 2.09999993443489E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 226, "col": 84, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 54358, "time": 5.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 226, "check_col": 84, "msg_id": 139, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 226, "col": 84, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 53154, "time": 4.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 226, "check_col": 84, "msg_id": 140, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 226, "col": 101, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5796, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 226, "check_col": 101, "msg_id": 141, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 226, "col": 45, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { }, "transformations": { "trivial_true": [ ] } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 19611, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4373, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4373, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 54181, "time": 4.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 53246, "time": 5.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 226, "check_col": 45, "msg_id": 142, "session_dir": 10, "how_proved": "prover", "stats": { "Trivial": { "count": 1, "max_steps": 0, "max_time": 0.00000000000000E+00 }, "Z3": { "count": 5, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 225, "col": 50, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5770, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 225, "check_col": 50, "msg_id": 143, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 250, "col": 48, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 59967, "time": 4.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 250, "check_col": 48, "msg_id": 144, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 250, "col": 48, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 99654, "time": 5.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4141, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 250, "check_col": 48, "msg_id": 145, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 250, "col": 13, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 63407, "time": 5.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 91997, "time": 6.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 250, "check_col": 13, "msg_id": 146, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 5.99999986588955E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 251, "col": 19, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { }, "transformations": { "trivial_true": [ ] } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5718, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 56153, "time": 3.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 173075, "time": 1.55000000000000E+00 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 173075, "time": 1.54000000000000E+00 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 14955, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4129, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 251, "check_col": 19, "msg_id": 147, "session_dir": 10, "how_proved": "prover", "stats": { "CVC4": { "count": 2, "max_steps": 4517, "max_time": 1.54999995231628E+00 }, "Trivial": { "count": 1, "max_steps": 0, "max_time": 0.00000000000000E+00 }, "Z3": { "count": 4, "max_steps": 1, "max_time": 2.99999993294477E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 245, "col": 58, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 44373, "time": 3.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 106652, "time": 5.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 245, "check_col": 58, "msg_id": 148, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 245, "col": 52, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 174427, "time": 8.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 245, "check_col": 52, "msg_id": 149, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 7.99999982118607E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 245, "col": 38, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 11918, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 245, "check_col": 38, "msg_id": 150, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 246, "col": 38, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 14240, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 246, "check_col": 38, "msg_id": 151, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 248, "col": 59, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 14543, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 248, "check_col": 59, "msg_id": 152, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 248, "col": 39, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { }, "transformations": { "trivial_true": [ ] } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 17900, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 12408, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 12408, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 12382, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 14514, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 248, "check_col": 39, "msg_id": 153, "session_dir": 10, "how_proved": "prover", "stats": { "Trivial": { "count": 1, "max_steps": 0, "max_time": 0.00000000000000E+00 }, "Z3": { "count": 5, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 258, "col": 36, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4635, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 258, "check_col": 36, "msg_id": 154, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 258, "col": 13, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 58440, "time": 5.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 188490, "time": 9.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 258, "check_col": 13, "msg_id": 155, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 9.00000035762787E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 259, "col": 47, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6385, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 259, "check_col": 47, "msg_id": 156, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 9.99999977648258E-03 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 259, "col": 71, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 97074, "time": 6.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 259, "check_col": 71, "msg_id": 157, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 5.99999986588955E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 259, "col": 83, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 60311, "time": 5.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 259, "check_col": 83, "msg_id": 158, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 259, "col": 83, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 99601, "time": 6.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 259, "check_col": 83, "msg_id": 159, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 5.99999986588955E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 259, "col": 88, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 100062, "time": 6.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 259, "check_col": 88, "msg_id": 160, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 5.99999986588955E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 259, "col": 58, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 62293, "time": 5.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 259, "check_col": 58, "msg_id": 161, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 259, "col": 58, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 151084, "time": 8.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 259, "check_col": 58, "msg_id": 162, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 7.99999982118607E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 259, "col": 19, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { }, "transformations": { "trivial_true": [ ] } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4785, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 66047, "time": 5.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 598266, "time": 5.89000000000000E+00 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 598266, "time": 5.91000000000000E+00 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 4764, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 66031, "time": 5.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 259, "check_col": 19, "msg_id": 163, "session_dir": 10, "how_proved": "prover", "stats": { "CVC4": { "count": 2, "max_steps": 16665, "max_time": 5.90999984741211E+00 }, "Trivial": { "count": 1, "max_steps": 0, "max_time": 0.00000000000000E+00 }, "Z3": { "count": 4, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 257, "col": 56, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 6726, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 54789, "time": 4.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 257, "check_col": 56, "msg_id": 164, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 257, "col": 80, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 67575, "time": 5.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13477, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 257, "check_col": 80, "msg_id": 165, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 257, "col": 92, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 27588, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13564, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 257, "check_col": 92, "msg_id": 166, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 257, "col": 92, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 67881, "time": 7.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13641, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 257, "check_col": 92, "msg_id": 167, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 7.00000002980232E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 257, "col": 97, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 68129, "time": 5.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 13796, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 257, "check_col": 97, "msg_id": 168, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 257, "col": 67, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 68427, "time": 5.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 24993, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 257, "check_col": 67, "msg_id": 169, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 257, "col": 67, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 150308, "time": 7.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 101594, "time": 7.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 257, "check_col": 67, "msg_id": 170, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 7.00000002980232E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 257, "col": 36, "rule": "VC_LOOP_INVARIANT_PRESERV", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 22836, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 257, "check_col": 36, "msg_id": 171, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 257, "col": 36, "rule": "VC_LOOP_INVARIANT_INIT", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 20132, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 257, "check_col": 36, "msg_id": 172, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 255, "col": 46, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 62954, "time": 5.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 255, "check_col": 46, "msg_id": 173, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 5.00000007450581E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 255, "col": 29, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 72649, "time": 6.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 255, "check_col": 29, "msg_id": 174, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 5.99999986588955E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 282, "col": 48, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 111130, "time": 1.00000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 282, "check_col": 48, "msg_id": 175, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.00000001490116E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 282, "col": 48, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "CVC4": { "result": "Timeout", "steps": -1, "time": 120 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 }, "altergo": { "result": "Valid", "steps": 4074, "time": 2.97400000000000E-01 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5376, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 282, "check_col": 48, "msg_id": 176, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 }, "altergo": { "count": 1, "max_steps": 4075, "max_time": 2.97399997711182E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 282, "col": 13, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 23738, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 442489, "time": 1.80000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 282, "check_col": 13, "msg_id": 177, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.80000007152557E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 277, "col": 38, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 15322, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 277, "check_col": 38, "msg_id": 178, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 278, "col": 61, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 22016, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 329402, "time": 1.10000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 278, "check_col": 61, "msg_id": 179, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 2, "max_steps": 1, "max_time": 1.09999999403954E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 278, "col": 55, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 583857, "time": 2.40000000000000E-01 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 278, "check_col": 55, "msg_id": 180, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 168, "max_time": 2.39999994635582E-01 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 278, "col": 38, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { }, "transformations": { "trivial_true": [ ] } }, { "proof_attempts": { "CVC4": { "result": "Valid", "steps": 1851151, "time": 2.66000000000000E+01 }, "Z3": { "result": "Timeout", "steps": -1, "time": 120 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 15645, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 15645, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 15633, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 15627, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 5142, "time": 1.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 278, "check_col": 38, "msg_id": 181, "session_dir": 10, "how_proved": "prover", "stats": { "CVC4": { "count": 1, "max_steps": 52462, "max_time": 2.66000003814697E+01 }, "Trivial": { "count": 1, "max_steps": 0, "max_time": 0.00000000000000E+00 }, "Z3": { "count": 5, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 280, "col": 79, "rule": "VC_RANGE_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 71819, "time": 8.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 280, "check_col": 79, "msg_id": 182, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 7.99999982118607E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 280, "col": 59, "rule": "VC_PRECONDITION", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { }, "transformations": { "trivial_true": [ ] } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 23096, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 16322, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 16322, "time": 1.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 16296, "time": 2.00000000000000E-02 } }, "transformations": { } }, { "proof_attempts": { "Z3": { "result": "Valid", "steps": 18888, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 280, "check_col": 59, "msg_id": 183, "session_dir": 10, "how_proved": "prover", "stats": { "Trivial": { "count": 1, "max_steps": 0, "max_time": 0.00000000000000E+00 }, "Z3": { "count": 5, "max_steps": 1, "max_time": 1.99999995529652E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 173, "col": 46, "rule": "VC_OVERFLOW_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 75112, "time": 4.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 173, "check_col": 46, "msg_id": 184, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 3.99999991059303E-02 } } }, { "file": "rflx-rflx_generic_types.adb", "line": 173, "col": 64, "rule": "VC_DIVISION_CHECK", "severity": "info", "entity": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] }, "check_tree": [ { "proof_attempts": { "Z3": { "result": "Valid", "steps": 3507, "time": 2.00000000000000E-02 } }, "transformations": { } } ], "check_file": "rflx-rflx_generic_types.adb", "check_line": 173, "check_col": 64, "msg_id": 185, "session_dir": 10, "how_proved": "prover", "stats": { "Z3": { "count": 1, "max_steps": 1, "max_time": 1.99999995529652E-02 } } } ], "assumptions": [ { "assumptions": [ { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } } ], "claim": { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Types.U64_Extract.D.ES", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 115 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } } ], "claim": { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract.D.ES", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 115 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } } ], "claim": { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Extract.D.ES", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 115 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.First_Bit_Index", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 38 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract.D.ES", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 115 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } ], "claim": { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.First_Bit_Index", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 38 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.Last_Bit_Index", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 41 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.Last_Bit_Index", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 41 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Insert.Read", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 184 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Insert.Read", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 184 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } ], "claim": { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } ], "claim": { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Utils.Mod_Pow2", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 35 } ] } }, { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Insert.Read", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 184 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Insert.Write", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 192 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Mod_Pow2", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 35 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Insert.Read", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 184 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Insert.Write", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 192 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Utils.Mod_Pow2", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 35 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } } ], "claim": { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Insert", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 166 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Extract.D", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 111 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Intermediate", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 43 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } ], "claim": { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Extract", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 92 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } } ], "claim": { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } } ], "claim": { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_POST", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Utils.Left_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 20 } ] } }, { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Utils.Right_Shift", "sloc": [ { "file": "rflx-rflx_utils.ads", "line": 10 } ] } } ], "claim": { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Extract_Remaining", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 68 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.U64_Insert.Write", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 192 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.U64_Insert.Write", "sloc": [ { "file": "rflx-rflx_generic_types.adb", "line": 192 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types", "sloc": [ { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.Unreachable_Bit_Length", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 65 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.Unreachable_Bit_Length", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 65 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_EFFECTS", "arg": { "name": "RFLX.RFLX_Types.Byte_Index", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 35 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } }, { "assumptions": [ ], "claim": { "predicate": "CLAIM_AORTE", "arg": { "name": "RFLX.RFLX_Types.Byte_Index", "sloc": [ { "file": "rflx-rflx_generic_types.ads", "line": 35 }, { "file": "rflx-rflx_types.ads", "line": 6 } ] } } } ], "timings": { "gnatwhy3.transformations.eliminate_algebraic": 1.06149995699525E-02, "gnatwhy3.transformations.inline_trivial": 9.73574066162109E+00, "codepeer results": 2.32999998843297E-04, "init_why_sections": 3.07999987853691E-04, "gnatwhy3.transformations.eliminate_let_term": 4.81700012460351E-03, "gnatwhy3.transformations.detect_polymorphism": 6.93240016698837E-02, "globals/properties (advanced)": 5.83000015467405E-04, "gnatwhy3.transformations.eliminate_literal": 1.86261996626854E-01, "gnatwhy3.run_vcs": 3.35460710525513E+00, "gnatwhy3.transformations.eliminate_definition_if_poly": 3.46079990267754E-02, "gnatwhy3.transformations.eliminate_algebraic_if_poly": 1.51537001132965E-01, "flow analysis": 7.23800016567111E-03, "gnatwhy3.transformations.simplify_formula": 2.98500001430511E-01, "marking": 4.80999995488673E-04, "translation of standard": 1.69699999969453E-03, "gnatwhy3.transformations.eliminate_recursion": 3.09900008141994E-03, "gnatwhy3.register_vcs": 1.41455399990082E+00, "gnatwhy3.transformations.eliminate_epsilon": 1.78152009844780E-01, "globals (basic)": 1.90999999176711E-04, "gnatwhy3.schedule_vcs": 2.96049993485212E-02, "gnatwhy3.transformations.prepare_for_counterexmp": 1.42999997478910E-04, "gnatwhy3.save_session": 1.10590003430843E-01, "gnatwhy3.transformations.eliminate_inductive": 1.20456002652645E-01, "gnatwhy3.transformations.split_premise_right": 1.06990002095699E-02, "gnatwhy3.transformations.encoding_smt_if_poly": 4.69999999040738E-04, "gnatwhy3.transformations.eliminate_unused_hypo": 1.87479362487793E+01, "gnatwhy3.transformations.eliminate_builtin": 1.60389006137848E-01, "gnatwhy3.transformations.discriminate_if_poly": 2.27100006304681E-03, "gnatwhy3.init": 2.27238702774048E+00, "gnatwhy3.transformations.introduce_premises": 2.02678585052490E+00 } }