- Reset encryption level issue.
This commit is contained in:
parent
08f705234b
commit
974e5f7315
@ -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
|
* @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;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -5,7 +5,6 @@
|
|||||||
|
|
||||||
#include <strings.h>
|
#include <strings.h>
|
||||||
#include "pheading.h"
|
#include "pheading.h"
|
||||||
#include "memory.h"
|
|
||||||
#include "tac.h"
|
#include "tac.h"
|
||||||
#include "switches.h"
|
#include "switches.h"
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user