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