diff --git a/src/arachne.c b/src/arachne.c index e1abd21..c7c70e7 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -2015,6 +2015,8 @@ prune_bounds () indentPrint (); eprintf ("Pruned: ran out of allowed time (-T %i switch)\n", get_time_limit () ); } + // Pruned because of time bound! + current_claim->timebound = 1; return 1; } diff --git a/src/compiler.c b/src/compiler.c index 90d9299..e4a13c5 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -548,6 +548,7 @@ commEvent (int event, Tac tc) cl->roledef = NULL; cl->count = 0; cl->complete = 0; + cl->timebound = 0; cl->failed = 0; cl->prec = NULL; cl->roles = NULL; diff --git a/src/main.c b/src/main.c index d1b19f5..a8c4e76 100644 --- a/src/main.c +++ b/src/main.c @@ -90,6 +90,9 @@ const char *releasetag = SVNVERSION " [modified]"; const char *releasetag = SVNVERSION; #endif +//! The number of seconds a test is allowed to run +static int time_limit_seconds; + //! The main body, as called by the environment. int main (int argc, char **argv) @@ -525,6 +528,7 @@ main (int argc, char **argv) sys->match = switch_match_method->ival[0]; mgu_match = sys->match; sys->prune = switch_pruning_method->ival[0]; + time_limit_seconds = switch_timer->ival[0]; set_time_limit (switch_timer->ival[0]); if (switch_progress_bar->count > 0) /* enable progress display */ @@ -826,9 +830,15 @@ timersPrint (const System sys) { eprintf ("\tcorrect: "); if (cl_scan->complete) - eprintf ("complete_proof"); + { + eprintf ("complete_proof"); + } else - eprintf ("bounded_proof"); + { + eprintf ("bounded_proof"); + if (cl_scan->timebound) + eprintf ("\ttime=%i",time_limit_seconds); + } } } else diff --git a/src/role.h b/src/role.h index 5e3f062..ba620c2 100644 --- a/src/role.h +++ b/src/role.h @@ -33,6 +33,8 @@ struct claimlist states_t failed; //! Whether the result is complete or not (failings always are!) int complete; + //! If we ran into the time bound (incomplete, and bad for results) + int timebound; int r; //!< role number for mapping int ev; //!< event index in role