Fix crashes with verification coverage + counterexamples (#817)

Previously, running Boogie with `/trackVerificationCoverage` and
`/enhancedErrorMessages:1` (or anything that leads to counterexample
parsing) would lead to crashes when verification failed. This fixes that
issue.

Source/Directory.Build.props

@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.0.7</Version>
+    <Version>3.0.8</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

Source/Model/ParserZ3.cs

@@ -281,6 +281,9 @@ internal override void Run()
           }
           else
           {
+            if (funName.StartsWith("aux$$")) {
+              continue;
+            }
             var fn = currModel.MkFunc(funName, 0);
             fn.SetConstant(GetElt(lastWord));
           }

Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs

@@ -186,7 +186,9 @@ private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
 
         if (options.LibOptions.ProduceUnsatCores) {
           var unsatCoreSExp = responseStack.Pop();
-          ReportCoveredElements(unsatCoreSExp);
+          if (result == Outcome.Valid) {
+            ReportCoveredElements(unsatCoreSExp);
+          }
         }
 
         if (result == Outcome.Invalid) {

Source/Provers/SMTLib/SMTLibProcess.cs

@@ -226,6 +226,8 @@ private async Task<SExpr> GetProverResponse()
               return resp;
             } else if (resp.Arguments[0].Name.Contains("model is not available")) {
               return null;
+            } else if (resp.Arguments[0].Name.Contains("unsat core is not available")) {
+              return null;
             } else if (resp.Arguments[0].Name.Contains("context is unsatisfiable")) {
               return null;
             } else if (resp.Arguments[0].Name.Contains("Cannot get model")) {

Test/coverage/verificationCoverageCounterexample.bpl

@@ -0,0 +1,6 @@
+// RUN: %boogie /trackVerificationCoverage /enhancedErrorMessages:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure P(x: int) {
+  assume {:id "id1"} x < 100;
+  assert {:id "id2"} x < 10;
+}

Test/coverage/verificationCoverageCounterexample.bpl.expect

@@ -0,0 +1,5 @@
+verificationCoverageCounterexample.bpl(5,3): Error: this assertion could not be proved
+Execution trace:
+    verificationCoverageCounterexample.bpl(4,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error