Quantifier regression tests: ensure full conversion

Test for the absence of warnings about failed conversion. Two regression tests
fail with this added check.

Author: tautschnig

regression/cbmc/Quantifiers-assertion/test.desc

@@ -12,3 +12,5 @@ main.c
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/Quantifiers-assignment/test.desc

@@ -10,3 +10,5 @@ main.c
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/Quantifiers-copy/test.desc

@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/Quantifiers-if/test.desc

@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/Quantifiers-initialisation/test.desc

@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/Quantifiers-initialisation2/test.desc

@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/Quantifiers-invalid-var-range/test.desc

@@ -1,8 +1,13 @@
-CORE
+KNOWNBUG
 main.c
 
 ^\*\* Results:$
 ^\*\* 0 of 1 failed
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
+--
+^warning: ignoring
+--
+This produces the expected verification result, but actually ignores some
+quantifiers.

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

@@ -12,3 +12,5 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/Quantifiers-not/test.desc

@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring

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

@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/Quantifiers-type/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^\*\* Results:$
@@ -8,3 +8,8 @@ main.c
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring
+--
+This produces the expected verification result, but actually ignores some
+quantifiers.

regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc

@@ -5,3 +5,4 @@ quantifier-with-side-effect.c
 ^SIGNAL=0$
 ^file .* line 10 function main: quantifier must not contain side effects$
 --
+^warning: ignoring