diff --git a/src/arachne.c b/src/arachne.c index b9c0d65..dff449d 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -1253,6 +1253,9 @@ bind_goal_new_intruder_run (const Binding b) } //! Bind a regular goal +/** + * Problem child. Valgrind does not like it. + */ int bind_goal_regular_run (const Binding b) { @@ -1292,7 +1295,7 @@ bind_goal_regular_run (const Binding b) if (!termMguSubTerm (b->term, rd->message, test_sub_unification, sys->know->inverses, NULL)) { - int flag; + int sflag; // A good candidate found++; @@ -1317,11 +1320,11 @@ bind_goal_regular_run (const Binding b) } indentDepth++; // Bind to existing run - flag = bind_existing_run (b, p, r, index); + sflag = bind_existing_run (b, p, r, index); // bind to new run - flag = flag && bind_new_run (b, p, r, index); + sflag = sflag && bind_new_run (b, p, r, index); indentDepth--; - return flag; + return sflag; } else { @@ -1506,12 +1509,21 @@ prune_theorems () run = 1; while (run < sys->maxruns) { - if (inTermlist (sys->untrusted, agentOfRun (sys, run))) + if (sys->runs[run].protocol != INTRUDER) { - if (sys->output == PROOF) + Term actor; + + actor = agentOfRun(sys, run); + eprintf ("Bla %i ", run); + termPrint (actor); + eprintf ("\n"); + if (inTermlist (sys->untrusted, actor)) { - indentPrint (); - eprintf ("Pruned because the actor of run %i is untrusted.\n", run); + if (sys->output == PROOF) + { + indentPrint (); + eprintf ("Pruned because the actor of run %i is untrusted.\n", run); + } } } run++; diff --git a/src/system.c b/src/system.c index d3a3966..78e8ca7 100644 --- a/src/system.c +++ b/src/system.c @@ -339,15 +339,22 @@ agentOfRunRole (const System sys, const int run, const Term role) Termlist agents = sys->runs[run].agents; /* TODO stupid reversed order, lose that soon */ - agents = termlistForward (agents); - while (agents != NULL && roles != NULL) + if (agents != NULL) { - if (isTermEqual (roles->term, role)) + agents = termlistForward (agents); + while (agents != NULL && roles != NULL) { - return agents->term; + if (isTermEqual (roles->term, role)) + { + return agents->term; + } + agents = agents->prev; + roles = roles->next; } - agents = agents->prev; - roles = roles->next; + } + else + { + error ("Agent list for run %i is empty, so agentOfRunRole is not usable.", run); } return NULL; }