From a4429d548f228c92cf5f291e2dbb7aefb5930223 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Tue, 28 Feb 2006 13:57:38 +0000
Subject: [PATCH] - Turned 'hidden' term lemma back on by default.

---
 src/prune_theorems.c | 25 +++++++++++--------------
 1 file changed, 11 insertions(+), 14 deletions(-)

diff --git a/src/prune_theorems.c b/src/prune_theorems.c
index ea92f6d..d0ee503 100644
--- a/src/prune_theorems.c
+++ b/src/prune_theorems.c
@@ -296,7 +296,7 @@ prune_theorems (const System sys)
   /*
    * Check for correct orderings involving local constants
    */
-  if (switches.experimental & 8)
+  if (!(switches.experimental & 8))
     {
       if (!correctLocalOrder (sys))
 	{
@@ -320,22 +320,19 @@ prune_theorems (const System sys)
 
       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
-	  //!@TODO in the future, this can be subsumed by adding TERM_Hidden to the hidelevel constructs
-	  if (termInTerm (b->term, TERM_Hidden))
+	  // Prune the state: we can never meet this
+	  if (switches.output == PROOF)
 	    {
-	      // Prune the state: we can never meet this
-	      if (switches.output == PROOF)
-		{
-		  indentPrint ();
-		  eprintf ("Pruned because intruder can never construnct ");
-		  termPrint (b->term);
-		  eprintf ("\n");
-		}
-	      return true;
+	      indentPrint ();
+	      eprintf ("Pruned because intruder can never construnct ");
+	      termPrint (b->term);
+	      eprintf ("\n");
 	    }
+	  return true;
 	}
 
       if (switches.experimental & 4)