From 73acc8f60b21c58e00eaf2c6be31913f464f5e1e Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 25 Dec 2024 17:36:48 +0100 Subject: [PATCH] chore: add timeout for long-running files (#912) --- SSA/Projects/InstCombine/TacticAuto.lean | 4 ++-- bv-evaluation/compare-leansat-vs-bitwuzla-llvm-sym.py | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean index 6210b919f..5645d31fc 100644 --- a/SSA/Projects/InstCombine/TacticAuto.lean +++ b/SSA/Projects/InstCombine/TacticAuto.lean @@ -300,8 +300,8 @@ macro "bv_bench": tactic => "bv_normalize" : (bv_normalize; done), "bv_decide" : (bv_decide; done), "bv_auto" : (bv_auto; done), - "bv_automata_circuit" : (bv_automata_circuit (config := { circuitSizeThreshold := 30 } ); done), - "bv_normalize_automata_circuit" : ((try (solve | bv_normalize)); (try bv_automata_circuit (config := { circuitSizeThreshold := 30 } )); done) + "bv_automata_circuit" : (bv_automata_circuit; done), + "bv_normalize_automata_circuit" : ((try (solve | bv_normalize)); (try bv_automata_circuit); done) ] try bv_auto try sorry diff --git a/bv-evaluation/compare-leansat-vs-bitwuzla-llvm-sym.py b/bv-evaluation/compare-leansat-vs-bitwuzla-llvm-sym.py index 712f23f5f..1dcdfe1d2 100644 --- a/bv-evaluation/compare-leansat-vs-bitwuzla-llvm-sym.py +++ b/bv-evaluation/compare-leansat-vs-bitwuzla-llvm-sym.py @@ -33,7 +33,7 @@ def run_file(file: str): with open(log_file_path, 'w') as log_file: cmd = 'lake lean ' + file_path print(cmd) - subprocess.Popen(cmd, cwd=ROOT_DIR, stdout=log_file, stderr=log_file, shell=True).wait() + subprocess.Popen(cmd, cwd=ROOT_DIR, stdout=log_file, stderr=log_file, shell=True).wait(timeout=1800) subprocess.Popen('sed -i -E \'s,bv_bench,simp_alive_benchmark,g\' ' + file_path, cwd=ROOT_DIR, shell=True).wait() def process(jobs: int):