From acb89922f1acc4390f5686858a0773ce00055f10 Mon Sep 17 00:00:00 2001 From: ccremers Date: Sat, 28 Aug 2004 12:20:50 +0000 Subject: [PATCH] - Singular variables need to be bound as well (to ensure ordering is correct w.r.t. e.g. nonces, if the intruder cannot construct them.) --- src/arachne.c | 45 +++++++++++++++++++-------------------------- 1 file changed, 19 insertions(+), 26 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 67a482b..7ce464a 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -898,38 +898,31 @@ select_goal () b = (Binding) bl->data; if (!b->done) { - // We don't care about singular variables. - /** - * Note that to mirror the modelchecker semantics, we should check whether the type exists in M_0. - */ - if (!isTermVariable (b->term)) - { - float cons; + float cons; - if (sys->output == PROOF && best != NULL) - eprintf (", "); - if (b->level >= max_level) + if (sys->output == PROOF && best != NULL) + eprintf (", "); + if (b->level >= max_level) + { + if (b->level > max_level) { - if (b->level > max_level) - { - max_level = b->level; - min_constrain = 1; // 1 is the maximum - } - cons = term_constrain_level (b->term); - if (cons <= min_constrain) - { - min_constrain = cons; - best = b; - if (sys->output == PROOF) - eprintf ("*"); - } + max_level = b->level; + min_constrain = 1; // 1 is the maximum } - if (sys->output == PROOF) + cons = term_constrain_level (b->term); + if (cons <= min_constrain) { - termPrint (b->term); - eprintf ("[%i]", b->level); + min_constrain = cons; + best = b; + if (sys->output == PROOF) + eprintf ("*"); } } + if (sys->output == PROOF) + { + termPrint (b->term); + eprintf ("[%i]", b->level); + } } bl = bl->next; }