By failing to check states whose hashes already appeared in the model
checker table, the datasheet test was missing some bugs. This commit
changes the datasheet test code to check the state before it checks for
the hash.
assert (n_rows < MAX_ROWS);
assert (n_columns < MAX_COLS);
assert (n_rows < MAX_ROWS);
assert (n_columns < MAX_COLS);
- /* If it is a duplicate hash, discard the state before checking
- its consistency, to save time. */
- if (mc_discard_dup_state (mc, hash_datasheet (ds)))
- {
- datasheet_destroy (ds);
- return;
- }
-
/* Check contents of datasheet via datasheet functions. */
if (!check_caseproto (mc, proto, datasheet_get_proto (ds), "datasheet"))
{
/* Check contents of datasheet via datasheet functions. */
if (!check_caseproto (mc, proto, datasheet_get_proto (ds), "datasheet"))
{
"have been (size %zu,%zu)", n_rows, n_columns);
}
"have been (size %zu,%zu)", n_rows, n_columns);
}
+ if (mc_discard_dup_state (mc, hash_datasheet (ds)))
+ datasheet_destroy (ds);
+ else
+ mc_add_state (mc, ds);
}
/* Extracts the contents of DS into DATA. */
}
/* Extracts the contents of DS into DATA. */