[[11, ["JType_JInd_Oma", "JType_JInd_Progress", "JType_JInd_Stall"], "rIC3 -e kind --no-preproc", [20, 12.79208755493164, 44.57916307449341, "OK", "RESULT: UNSAT\n", "[INFO ] the model to be checked: /home/louis-emile/OS-formal-ibex/dv/formal/build/aiger-277.aig\n[WARN ] multiple properties detected. rIC3 has compressed them into a single property\n[INFO ] origin ts has 9204841 vars, 1372396 inputs, 6882 latches, 12720195 clauses, 408 constraints\n[WARN ] Kind does not currently detect counter-example. Please run BMC separately or use the portfolio mode if needed.\n[INFO ] kind depth: 1\n[INFO ] k-induction proofed in depth 1\n"]], [11, ["Mem_ExcCSRMaintainEx"], "rIC3 -e kind --no-preproc", [20, 13.926959991455078, 174.55626964569092, "OK", "RESULT: UNSAT\n", "[INFO ] the model to be checked: /home/louis-emile/OS-formal-ibex/dv/formal/build/aiger-87.aig\n[INFO ] origin ts has 9205952 vars, 1372396 inputs, 6882 latches, 12722078 clauses, 408 constraints\n[WARN ] Kind does not currently detect counter-example. Please run BMC separately or use the portfolio mode if needed.\n[INFO ] kind depth: 1\n[INFO ] k-induction proofed in depth 1\n"]], [11, ["Mem_PCMaintainEx1", "Mem_PCMaintainEx2", "Mem_PMPErrMatch"], "rIC3 -e kind --no-preproc", [20, 16.043071746826172, 146.65763664245605, "OK", "RESULT: UNSAT\n", "[INFO ] the model to be checked: /home/louis-emile/OS-formal-ibex/dv/formal/build/aiger-104.aig\n[WARN ] multiple properties detected. rIC3 has compressed them into a single property\n[INFO ] origin ts has 9205097 vars, 1372396 inputs, 6882 latches, 12720638 clauses, 408 constraints\n[WARN ] Kind does not currently detect counter-example. Please run BMC separately or use the portfolio mode if needed.\n[INFO ] kind depth: 1\n[INFO ] k-induction proofed in depth 1\n"]], [11, ["Mem_LSU2ndReqStep", "Mem_LSUEarlyRequestSplit", "Mem_LSUHold", "Mem_LSUHoldWrite", "Mem_LSUInternalHold", "Mem_LSULateRespFinishing", "Mem_LSUMaxTwoReqs"], "rIC3 -e kind --no-preproc", [20, 12.99798583984375, 52.52440404891968, "OK", "RESULT: UNSAT\n", "[INFO ] the model to be checked: /home/louis-emile/OS-formal-ibex/dv/formal/build/aiger-257.aig\n[WARN ] multiple properties detected. rIC3 has compressed them into a single property\n[INFO ] origin ts has 9206480 vars, 1372526 inputs, 6882 latches, 12723102 clauses, 408 constraints\n[WARN ] Kind does not currently detect counter-example. Please run BMC separately or use the portfolio mode if needed.\n[INFO ] kind depth: 1\n[INFO ] k-induction proofed in depth 1\n"]], [11, ["Mem_AltLSUVeryEarly"], "rIC3 -e kind --no-preproc", [20, 13.10592269897461, 43.578543186187744, "OK", "RESULT: UNSAT\n", "[INFO ] the model to be checked: /home/louis-emile/OS-formal-ibex/dv/formal/build/aiger-133.aig\n[INFO ] origin ts has 9208291 vars, 1372780 inputs, 6882 latches, 12726133 clauses, 408 constraints\n[WARN ] Kind does not currently detect counter-example. Please run BMC separately or use the portfolio mode if needed.\n[INFO ] kind depth: 1\n[INFO ] k-induction proofed in depth 1\n"]], [11, ["Mem_CSRMaintainEx"], "rIC3 -e kind --no-preproc", [20, 13.90517807006836, 179.08196568489075, "OK", "RESULT: UNSAT\n", "[INFO ] the model to be checked: /home/louis-emile/OS-formal-ibex/dv/formal/build/aiger-77.aig\n[INFO ] origin ts has 9206480 vars, 1372396 inputs, 6882 latches, 12723002 clauses, 408 constraints\n[WARN ] Kind does not currently detect counter-example. Please run BMC separately or use the portfolio mode if needed.\n[INFO ] kind depth: 1\n[INFO ] k-induction proofed in depth 1\n"]], [11, ["BType_BInd_Oma", "BType_BInd_Progress", "BType_BInd_Stall"], "rIC3 -e kind --no-preproc", [20, 12.791057586669922, 40.396634578704834, "OK", "RESULT: UNSAT\n", "[INFO ] the model to be checked: /home/louis-emile/OS-formal-ibex/dv/formal/build/aiger-278.aig\n[WARN ] multiple properties detected. rIC3 has compressed them into a single property\n[INFO ] origin ts has 9204841 vars, 1372396 inputs, 6882 latches, 12720195 clauses, 408 constraints\n[WARN ] Kind does not currently detect counter-example. Please run BMC separately or use the portfolio mode if needed.\n[INFO ] kind depth: 1\n[INFO ] k-induction proofed in depth 1\n"]], [11, ["Mem_NoMem"], "rIC3 -e kind --no-preproc", [20, 12.660163879394531, 31.4222092628479, "OK", "RESULT: UNSAT\n", "[INFO ] the model to be checked: /home/louis-emile/OS-formal-ibex/dv/formal/build/aiger-295.aig\n[INFO ] origin ts has 9204758 vars, 1372396 inputs, 6882 latches, 12719946 clauses, 408 constraints\n[WARN ] Kind does not currently detect counter-example. Please run BMC separately or use the portfolio mode if needed.\n[INFO ] kind depth: 1\n[INFO ] k-induction proofed in depth 1\n"]]]