- Fixed some stupid maxAttacks handling. Note that it still needs to

improve (todo list).
This commit is contained in:
ccremers 2006-08-15 08:16:02 +00:00
parent 04b03d7664
commit b5470aa894
3 changed files with 15 additions and 4 deletions

View File

@ -821,10 +821,6 @@ property_check (const System sys)
flag = 1; flag = 1;
/* Do we need any? */
if (enoughAttacks (sys))
return flag;
/** /**
* By the way the claim is handled, this automatically means a flaw. * By the way the claim is handled, this automatically means a flaw.
*/ */

View File

@ -45,6 +45,19 @@ prune_bounds (const System sys)
return 1; 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 */ /* prune for proof depth */
if (proofDepth > switches.maxproofdepth) if (proofDepth > switches.maxproofdepth)
{ {

View File

@ -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 - There is something weird when automatically generating claim labels
and trying to filter on them (try eg duplicates) and trying to filter on them (try eg duplicates)
- --check is slightly f***ed up because there is no good semantics for - --check is slightly f***ed up because there is no good semantics for