summaryrefslogtreecommitdiff
path: root/src/counterexample.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/counterexample.c')
-rw-r--r--src/counterexample.c15
1 files changed, 12 insertions, 3 deletions
diff --git a/src/counterexample.c b/src/counterexample.c
index 8a4f8b2c..82ee43da 100644
--- a/src/counterexample.c
+++ b/src/counterexample.c
@@ -30,6 +30,7 @@
#include <gl_rbtreehash_list.h>
#include <hash.h>
#include <mbswidth.h>
+#include <quote.h>
#include <stdlib.h>
#include <textstyle.h>
#include <time.h>
@@ -1209,15 +1210,23 @@ static xtime_t cumulative_time;
void
counterexample_init (void)
{
+ // Check cex.timeout.
{
- char *cp = muscle_percent_define_get ("cex.timeout");
+ const char *variable = "cex.timeout";
+ char *cp = muscle_percent_define_get (variable);
if (*cp != '\0')
{
char *end = NULL;
double v = c_strtod (cp, &end);
- if (*end == '\0' && errno == 0)
+ if (*end == '\0' && errno == 0 && v >= 0)
time_limit = v;
- fprintf (stderr, "lim: %f from %s\n", time_limit, cp);
+ else
+ {
+ location loc = muscle_percent_define_get_loc (variable);
+ complain (&loc, complaint,
+ _("invalid value for %%define variable %s: %s"),
+ quote (variable), quote_n (1, cp));
+ }
}
free (cp);
}