[[14, ["JType_Jal_Addr", "JType_Jal_CSR", "JType_Jal_Data", "JType_Jal_PC"], "rIC3 -e kind --no-preproc", [20, 13.930557250976562, 124.74911975860596, "OK", "RESULT: UNSAT\n", "[INFO ] the model to be checked: /home/louis-emile/OS-formal-ibex/dv/formal/build/aiger-152.aig\n[WARN ] multiple properties detected. rIC3 has compressed them into a single property\n[INFO ] origin ts has 9226734 vars, 1373680 inputs, 6882 latches, 12760927 clauses, 454 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"]], [14, ["JType_Jalr_Addr", "JType_Jalr_CSR", "JType_Jalr_Data", "JType_Jalr_PC"], "rIC3 -e kind --no-preproc", [20, 16.389507293701172, 222.60614895820618, "OK", "RESULT: UNSAT\n", "[INFO ] the model to be checked: /home/louis-emile/OS-formal-ibex/dv/formal/build/aiger-106.aig\n[WARN ] multiple properties detected. rIC3 has compressed them into a single property\n[INFO ] origin ts has 9226746 vars, 1373680 inputs, 6882 latches, 12760963 clauses, 454 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"]], [14, ["Mem_Load_En", "Mem_Load_NoWe", "Mem_Store_We", "Mem_Store_En"], "rIC3 -e kind --no-preproc", [20, 12.87420654296875, 20.385092973709106, "OK", "RESULT: UNSAT\n"]]]