From b5036a4baa02cac62a29312065b546a0a3759124 Mon Sep 17 00:00:00 2001 From: Douglas Stebila Date: Mon, 14 Mar 2022 16:26:30 -0400 Subject: [PATCH] Missing some lemmas in run_proofs script --- run_proofs.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/run_proofs.py b/run_proofs.py index fc3135d..4e5fe3c 100644 --- a/run_proofs.py +++ b/run_proofs.py @@ -32,9 +32,9 @@ def run_tamarin(model: str, prove: Union[str, None], defines: List[str]) -> str: return result.stdout -def get_lemmas(model: str) -> Iterable[str]: +def get_lemmas(model: str, defines) -> Iterable[str]: """Parse out the lemmas from the output of Tamarin""" - lines = run_tamarin(model, None, []).splitlines() + lines = run_tamarin(model, None, defines).splitlines() for line in lines: if m := LEMMA_REGEX.match(line): @@ -76,7 +76,7 @@ def prove_lemmas(model, lemmas: Iterable[str], defines): model = sys.argv[1] defines = sys.argv[2:] - lemmas = get_lemmas(model) + lemmas = get_lemmas(model, defines) start_time = datetime.now() prove_lemmas(model, lemmas, defines) duration = datetime.now() - start_time