enum-trace1 regression test: ensure inputs are sane

The test descriptions expect valid enum values, which we didn't actually
have any guarantee built into the test for.

Author: tautschnig

regression/cbmc/enum-trace1/main.c

@@ -16,6 +16,9 @@ typedef enum ENUMT
 
 void test(enum ENUM e, enum_t t)
 {
+  // ensure sane input values
+  __CPROVER_assume(__CPROVER_enum_is_in_range(e));
+  __CPROVER_assume(__CPROVER_enum_is_in_range(t));
   enum ENUM ee = e;
   enum_t tt = t;