make tests more easily satisfiable

Author: Daniel Kroening

regression/cbmc/Quantifiers-copy/test.desc

@@ -2,11 +2,11 @@ CORE
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] assertion b\[(signed long int)0\] == 0: SUCCESS$
-^\[main.assertion.2\] assertion b\[(signed long int)1\] == 1: SUCCESS$
-^\[main.assertion.3\] assertion b\[(signed long int)2\] == 2: SUCCESS$
-^\[main.assertion.4\] assertion b\[(signed long int)3\] == 3: SUCCESS$
-^\[main.assertion.5\] assertion b\[(signed long int)4\] == 4: SUCCESS$
+^\[main.assertion.1\] assertion b\[.*\] == 0: SUCCESS$
+^\[main.assertion.2\] assertion b\[.*\] == 1: SUCCESS$
+^\[main.assertion.3\] assertion b\[.*\] == 2: SUCCESS$
+^\[main.assertion.4\] assertion b\[.*\] == 3: SUCCESS$
+^\[main.assertion.5\] assertion b\[.*\] == 4: SUCCESS$
 
 ^\*\* 0 of 5 failed (1 iteration)$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Quantifiers-initialisation/test.desc

@@ -2,11 +2,11 @@ CORE
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] assertion a\[(signed long int)0\] == 1: SUCCESS$
-^\[main.assertion.2\] assertion a\[(signed long int)1\] == 2: SUCCESS$
-^\[main.assertion.3\] assertion a\[(signed long int)2\] == 3: SUCCESS$
-^\[main.assertion.4\] assertion a\[(signed long int)3\] == 4: SUCCESS$
-^\[main.assertion.5\] assertion a\[(signed long int)4\] == 5: SUCCESS$
+^\[main.assertion.1\] assertion a\[.*\] == 1: SUCCESS$
+^\[main.assertion.2\] assertion a\[.*\] == 2: SUCCESS$
+^\[main.assertion.3\] assertion a\[.*\] == 3: SUCCESS$
+^\[main.assertion.4\] assertion a\[.*\] == 4: SUCCESS$
+^\[main.assertion.5\] assertion a\[.*\] == 5: SUCCESS$
 
 ^\*\* 0 of 5 failed (1 iteration)$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Quantifiers-initialisation2/test.desc

@@ -3,10 +3,10 @@ main.c
 
 ^\*\* Results:$
 ^\[main.assertion.1\] forall a\[\]: SUCCESS$
-^\[main.assertion.2\] assertion a\[(signed long int)9\] > a\[(signed long int)1\]: SUCCESS$
-^\[main.assertion.3\] assertion a\[(signed long int)2\] > a\[(signed long int)3\]: FAILURE$
+^\[main.assertion.2\] assertion a\[.*\] > a\[.*\]: SUCCESS$
+^\[main.assertion.3\] assertion a\[.*\] > a\[.*\]: FAILURE$
 ^\[main.assertion.4\] forall c\[\]: SUCCESS$
-^\[main.assertion.5\] assertion c\[(signed long int)3\] >= c\[(signed long int)1\]: SUCCESS$
+^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$
 
 ^\*\* 1 of 5 failed (2 iterations)$
 ^VERIFICATION FAILED$

regression/cbmc/Quantifiers-not-exists/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] assertion a\[(signed long int)0\]\[(signed long int)0\] > 10: SUCCESS$
+^\[main.assertion.1\] assertion a\[.*\]\[.*\] > 10: SUCCESS$
 ^\[main.assertion.2\] assertion tmp_if_expr$3: SUCCESS$
 ^\[main.assertion.3\] assertion tmp_if_expr$6: SUCCESS$
 ^\[main.assertion.4\] assertion tmp_if_expr$9: SUCCESS$

regression/cbmc/Quantifiers-two-dimension-array/test.desc

@@ -2,10 +2,10 @@ CORE
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] assertion a\[(signed long int)0\]\[(signed long int)0\] == 0: SUCCESS$
-^\[main.assertion.2\] assertion a\[(signed long int)0\]\[(signed long int)1\] == 1: SUCCESS$
-^\[main.assertion.3\] assertion a\[(signed long int)1\]\[(signed long int)0\] == 1: SUCCESS$
-^\[main.assertion.4\] assertion a\[(signed long int)1\]\[(signed long int)1\] == 2: SUCCESS$
+^\[main.assertion.1\] assertion a\[.*\]\[.*\] == 0: SUCCESS$
+^\[main.assertion.2\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
+^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
+^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$
 ^\[main.assertion.5\] assertion tmp_if_expr$3: SUCCESS$
 
 ^\*\* 0 of 5 failed (1 iteration)$