[[12, ["Mem_AltLSUEarly", "Mem_PCNoChangeNoBranch"], "rIC3 -e kind --no-preproc", [20, 13.119216918945312, 69.39226651191711, "OK", "RESULT: UNSAT\n", "[INFO ] the model to be checked: /home/louis-emile/OS-formal-ibex/dv/formal/build/aiger-265.aig\n[WARN ] multiple properties detected. rIC3 has compressed them into a single property\n[INFO ] origin ts has 9217382 vars, 1373294 inputs, 6882 latches, 12742979 clauses, 428 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"]], [12, ["JType_Branch"], "rIC3 -e kind --no-preproc", [20, 16.043514251708984, 240.1651349067688, "OK", "RESULT: UNSAT\n", "[INFO ] the model to be checked: /home/louis-emile/OS-formal-ibex/dv/formal/build/aiger-83.aig\n[INFO ] origin ts has 9213834 vars, 1372910 inputs, 6882 latches, 12736712 clauses, 428 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"]], [12, ["BType_NoBranch"], "rIC3 -e kind --no-preproc", [20, 16.038925170898438, 463.7887578010559, "OK", "RESULT: UNSAT\n", "[INFO ] the model to be checked: /home/louis-emile/OS-formal-ibex/dv/formal/build/aiger-41.aig\n[INFO ] origin ts has 9213839 vars, 1372910 inputs, 6882 latches, 12736722 clauses, 428 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"]], [12, ["BType_Branch"], "rIC3 -e kind --no-preproc", [20, 16.076858520507812, 466.69943165779114, "OK", "RESULT: UNSAT\n", "[INFO ] the model to be checked: /home/louis-emile/OS-formal-ibex/dv/formal/build/aiger-46.aig\n[INFO ] origin ts has 9213839 vars, 1372910 inputs, 6882 latches, 12736722 clauses, 428 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"]]]