From 974e5f731578e9db87b40ef5430b21150d7b9c04 Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 13 Apr 2006 12:43:13 +0000 Subject: [PATCH] - Reset encryption level issue. --- src/prune_theorems.c | 12 ++++++++++-- src/scanner.l | 1 - 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/prune_theorems.c b/src/prune_theorems.c index 9d28782..4c4df1f 100644 --- a/src/prune_theorems.c +++ b/src/prune_theorems.c @@ -410,12 +410,20 @@ prune_theorems (const System sys) } } - // To be on the safe side, we currently limit the encryption level to two. This is not a problem for known attacks, but should be addressed more carefully at some point. + // To be on the safe side, we currently limit the encryption level. This is not a problem for known attacks, but should be addressed more carefully at some point. /** * @todo Fix untyped variables reasoning */ - if (term_encryption_level (b->term) > 2) + if (term_encryption_level (b->term) > max_encryption_level) { + // Prune: we do not need to construct such terms + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned because the encryption level of "); + termPrint (b->term); + eprintf (" is too high.\n"); + } return true; } diff --git a/src/scanner.l b/src/scanner.l index e8c4f10..5219934 100644 --- a/src/scanner.l +++ b/src/scanner.l @@ -5,7 +5,6 @@ #include #include "pheading.h" -#include "memory.h" #include "tac.h" #include "switches.h"