Fix regression tests failing after removing redundant if components

This commit fixes the regression tests failing because of the
optimization to the way `if` statements are translated to GOTO.

Specifically it fixes
 - the expected result of `--cover location` in 2 `cbmc-cover`
   regression tests
 - the index of blocks in 3 regression tests from `cbmc` and `cprover`.

Author: Enrico Steffinlongo

regression/cbmc-cover/block-coverage-report1/test.desc

@@ -3,9 +3,8 @@ main.c
 --cover location
 block 1 \(lines main.c:main:3,5\): SATISFIED
 block 2 \(lines main.c:main:6\): SATISFIED
-block 3 \(lines main.c:main:6,9\): FAILED
-block 4 \(lines main.c:main:8\): SATISFIED
-block 5 \(lines main.c:main:9\): SATISFIED
+block 3 \(lines main.c:main:8\): SATISFIED
+block 4 \(lines main.c:main:9\): SATISFIED
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc-cover/built-ins1/test.desc

@@ -3,7 +3,7 @@ main.c
 --cover location --unwind 1
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 5 of 8 covered
+^\*\* 5 of 7 covered
 --
 ^warning: ignoring
 ^\[.*<builtin-library-

regression/cbmc/destructors/compound_literal.desc

@@ -2,7 +2,7 @@ CORE new-smt-backend
 main.c
 --unwind 10 --show-goto-functions
 activate-multi-line-match
-(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*DEAD .*newAlloc0[\s]*(?P>comment_block)[\s]*DEAD .*pc[\s]*(?P>comment_block)[\s]*DEAD .*literal[\s]*(?P>comment_block)[\s]*9: END_FUNCTION
+(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*DEAD .*newAlloc0[\s]*(?P>comment_block)[\s]*DEAD .*pc[\s]*(?P>comment_block)[\s]*DEAD .*literal[\s]*(?P>comment_block)[\s]*8: END_FUNCTION
 ^EXIT=0$
 ^SIGNAL=0$
 --
@@ -16,7 +16,7 @@ Checks for:
        // 51 file main.c line 44 function main
        DEAD main::$tmp::literal
        // 52 file main.c line 45 function main
-    9: END_FUNCTION
+    8: END_FUNCTION
 
 This asserts that when you've created a compound literal that both temp and real
 variable gets killed.

regression/cbmc/destructors/enter_lexical_block.desc

@@ -2,15 +2,15 @@ CORE new-smt-backend
 main.c
 --unwind 10 --show-goto-functions
 activate-multi-line-match
-(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*6: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*GOTO 3
+(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*5: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*GOTO 3
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
 Checks for:
 
        // 37 file main.c line 36 function main
-    6: DECL main::1::2::2::newAlloc4 : struct tag-test
+    5: DECL main::1::2::2::newAlloc4 : struct tag-test
        // 38 file main.c line 36 function main
        ASSIGN main::1::2::2::newAlloc4 := { 4 }
        // 39 file main.c line 37 function main

regression/cprover/loops/while-break1.desc

@@ -3,15 +3,15 @@ while-break1.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S12in\(ς\)$
+^\(\d+\) ∀ ς : state \. S15T\(ς\) ⇒ S12in\(ς\)$
 ^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12in\(ς\)$
 ^\(\d+\) ∀ ς : state \. \(S12in\(ς\) ∧ ¬\(1 ≠ 0\)\) ⇒ S12T\(ς\)$
 ^\(\d+\) ∀ ς : state \. \(S12in\(ς\) ∧ 1 ≠ 0\) ⇒ S12\(ς\)$
-^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) = 0\)\) ⇒ S13T\(ς\)$
-^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ς\(❝main::1::x❞\) = 0\) ⇒ S13\(ς\)$
-^\(\d+\) ∀ ς : state \. S12T\(ς\) ⇒ S19in\(ς\)$
-^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ S19in\(ς\)$
-^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S19in\(ς\)$
+^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ς\(❝main::1::x❞\) = 0\) ⇒ S13T\(ς\)$
+^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) = 0\)\) ⇒ S13\(ς\)$
+^\(\d+\) ∀ ς : state \. S12T\(ς\) ⇒ S17in\(ς\)$
+^\(\d+\) ∀ ς : state \. S13T\(ς\) ⇒ S17in\(ς\)$
+^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17in\(ς\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
 --