diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index 3b6c7dc..b08195a 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -138,6 +138,11 @@ def run(mode, task, engine_idx, engine): proc_status = "FAIL" return None + if solver_args[0] == "rIC3": + match = re.match(r".*all workers unexpectedly exited.*", line) + if match: + proc_status = "ERROR" + if proc_status is not None: if not end_of_cex and not produced_cex and line.isdigit(): produced_cex = True diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 3d6d177..b155763 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -287,6 +287,9 @@ def run(mode, task, engine_idx, engine): match = re.match(r".*bmc found counter-example in depth (\d+).*", line) if match: common_state.current_step = int(match[1]) + match = re.match(r".*all workers unexpectedly exited.*", line) + if match: + common_state.solver_status = "error" if line == "UNSAT": if common_state.solver_status is None: common_state.solver_status = "unsat"