Check for unreachability before true / false in AI verification

There will be a few cases that were previously marked as either
"SUCCESS" or "FAILURE (if reachable)" that will now be marked as
"SUCCESS (unreachable)".  In the first case this is definitely an
improvement as it is more precise and generally people want to
know when assertions are safe just because they are unreachable.
In the second case it is a bit more debateable but I think that
saying "FAILURE (if reachable)" is kind of disengenuous when we
know that it isn't reachable.

Author: martin

regression/goto-analyzer/intervals_01/test.desc

@@ -6,7 +6,7 @@ main.c
 ^\[main.assertion.1\] line 7 assertion i\s*>=\s*10: SUCCESS$
 ^\[main.assertion.2\] line 10 assertion i\s*!=\s*30: SUCCESS$
 ^\[main.assertion.3\] line 13 assertion i\s*!=\s*15: UNKNOWN$
-^\[main.assertion.4\] line 16 assertion 0: SUCCESS$
+^\[main.assertion.4\] line 16 assertion 0: SUCCESS \(unreachable\)$
 ^\[main.assertion.5\] line 19 assertion j\s*>=\s*10: SUCCESS$
 ^\[main.assertion.6\] line 22 assertion i\s*>=\s*j: UNKNOWN$
 ^\[main.assertion.7\] line 25 assertion i\s*>=\s*11: SUCCESS$

regression/goto-analyzer/intervals_13/test.desc

@@ -6,7 +6,7 @@ main.c
 ^\[main.assertion.1\] line 7 assertion i\s*>=\s*10: SUCCESS$
 ^\[main.assertion.2\] line 10 assertion i\s*!=\s*30: SUCCESS$
 ^\[main.assertion.3\] line 13 assertion i\s*!=\s*15: UNKNOWN$
-^\[main.assertion.4\] line 16 assertion 0: SUCCESS$
+^\[main.assertion.4\] line 16 assertion 0: SUCCESS \(unreachable\)$
 ^\[main.assertion.5\] line 19 assertion j\s*>=\s*10: SUCCESS$
 ^\[main.assertion.6\] line 22 assertion i\s*>=\s*j: UNKNOWN$
 ^\[main.assertion.7\] line 25 assertion i\s*>=\s*11: SUCCESS$

src/goto-analyzer/static_verifier.cpp

@@ -307,7 +307,12 @@ bool static_verifier(
       results.push_back(static_verifier_resultt());
       auto &result = results.back();
 
-      if(e.is_true())
+      if(domain.is_bottom())
+      {
+        result.status = static_verifier_resultt::BOTTOM;
+        ++pass;
+      }
+      else if(e.is_true())
       {
         result.status = static_verifier_resultt::TRUE;
         ++pass;
@@ -317,11 +322,6 @@ bool static_verifier(
         result.status = static_verifier_resultt::FALSE;
         ++fail;
       }
-      else if(domain.is_bottom())
-      {
-        result.status = static_verifier_resultt::BOTTOM;
-        ++pass;
-      }
       else
       {
         result.status = static_verifier_resultt::UNKNOWN;