+ unsigned int fairwindow;
+ unsigned int enabledcount;
+ unsigned int bound;
+
+ /** @brief Maximum number of future values that can be sent to the same
+ * read */
+ int maxfuturevalues;
+
+ /** @brief Only generate a new future value/expiration pair if the
+ * expiration time exceeds the existing one by more than the slop
+ * value */
+ unsigned int expireslop;
+
+ /** @brief Verbosity (0 = quiet; 1 = noisy) */
+ int verbose;
+
+ /** @brief Command-line argument count to pass to user program */
+ int argc;
+
+ /** @brief Command-line arguments to pass to user program */
+ char **argv;
+};
+
+/** @brief Model checker execution stats */
+struct execution_stats {
+ int num_total; /**< @brief Total number of executions */
+ int num_infeasible; /**< @brief Number of infeasible executions */
+ int num_buggy_executions; /** @brief Number of buggy executions */
+ int num_complete; /**< @brief Number of feasible, non-buggy, complete executions */
+ int num_redundant; /**< @brief Number of redundant, aborted executions */