andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Turned 'hidden' term lemma back on by default.

Browse Source
This commit is contained in:
ccremers 2006-02-28 13:57:38 +00:00
parent 00616e45ed
commit a4429d548f
1 changed files with 11 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
src/prune_theorems.c
View File

@ -296,7 +296,7 @@ prune_theorems (const System sys)
/* /*
* Check for correct orderings involving local constants * Check for correct orderings involving local constants
*/ */
if (switches.experimental & 8) if (!(switches.experimental & 8))
{ {
if (!correctLocalOrder (sys)) if (!correctLocalOrder (sys))
{ {
@ -320,22 +320,19 @@ prune_theorems (const System sys)
b = bl->data; b = bl->data;
if (switches.experimental & 4) // Check for "Hidden" interm goals
//!@TODO in the future, this can be subsumed by adding TERM_Hidden to the hidelevel constructs
if (termInTerm (b->term, TERM_Hidden))
{ {
// Check for "Hidden" interm goals // Prune the state: we can never meet this
//!@TODO in the future, this can be subsumed by adding TERM_Hidden to the hidelevel constructs if (switches.output == PROOF)
if (termInTerm (b->term, TERM_Hidden))
{ {
// Prune the state: we can never meet this indentPrint ();
if (switches.output == PROOF) eprintf ("Pruned because intruder can never construnct ");
{ termPrint (b->term);
indentPrint (); eprintf ("\n");
eprintf ("Pruned because intruder can never construnct ");
termPrint (b->term);
eprintf ("\n");
}
return true;
} }
return true;
} }
if (switches.experimental & 4) if (switches.experimental & 4)