From b5470aa894eac3720b75af5a5e96a33f7e833e2c Mon Sep 17 00:00:00 2001 From: ccremers Date: Tue, 15 Aug 2006 08:16:02 +0000 Subject: [PATCH] - Fixed some stupid maxAttacks handling. Note that it still needs to improve (todo list). --- src/claim.c | 4 ---- src/prune_bounds.c | 13 +++++++++++++ src/todo.txt | 2 ++ 3 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/claim.c b/src/claim.c index e511a7a..12eac7a 100644 --- a/src/claim.c +++ b/src/claim.c @@ -821,10 +821,6 @@ property_check (const System sys) flag = 1; - /* Do we need any? */ - if (enoughAttacks (sys)) - return flag; - /** * By the way the claim is handled, this automatically means a flaw. */ diff --git a/src/prune_bounds.c b/src/prune_bounds.c index cbfa3ec..14b0aa5 100644 --- a/src/prune_bounds.c +++ b/src/prune_bounds.c @@ -45,6 +45,19 @@ prune_bounds (const System sys) return 1; } + /* prune for number of attacks */ + if (enoughAttacks (sys)) + { + // Oh no, we ran out of time! + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned: we already found the maximum number of attacks.\n"); + } + return 1; + } + /* prune for proof depth */ if (proofDepth > switches.maxproofdepth) { diff --git a/src/todo.txt b/src/todo.txt index 5ccb839..788d890 100644 --- a/src/todo.txt +++ b/src/todo.txt @@ -1,3 +1,5 @@ +- I've started on sanitizing the --max-attacks switch. It now prunes as a + bound, but it also needs to limit per-claim, I guess. - There is something weird when automatically generating claim labels and trying to filter on them (try eg duplicates) - --check is slightly f***ed up because there is no good semantics for