From 895bec512b607bcbab40d7e2f6c2e970ec4a6e17 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 27 Nov 2023 11:16:03 -0800
Subject: [PATCH 1/2] Fix crashes with coverage + counterexamples

---
 Source/Model/ParserZ3.cs                                    | 3 +++
 Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs           | 4 +++-
 Source/Provers/SMTLib/SMTLibProcess.cs                      | 2 ++
 Test/coverage/verificationCoverageCounterexample.bpl        | 6 ++++++
 Test/coverage/verificationCoverageCounterexample.bpl.expect | 5 +++++
 5 files changed, 19 insertions(+), 1 deletion(-)
 create mode 100644 Test/coverage/verificationCoverageCounterexample.bpl
 create mode 100644 Test/coverage/verificationCoverageCounterexample.bpl.expect

diff --git a/Source/Model/ParserZ3.cs b/Source/Model/ParserZ3.cs
index 222ee1611..157c69ec0 100644
--- a/Source/Model/ParserZ3.cs
+++ b/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));
           }
diff --git a/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs b/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs
index 9eb55bf64..9e434d272 100644
--- a/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs
+++ b/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) {
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 5a6211f45..5f09d0841 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/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")) {
diff --git a/Test/coverage/verificationCoverageCounterexample.bpl b/Test/coverage/verificationCoverageCounterexample.bpl
new file mode 100644
index 000000000..f0c8ae46c
--- /dev/null
+++ b/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;
+}
diff --git a/Test/coverage/verificationCoverageCounterexample.bpl.expect b/Test/coverage/verificationCoverageCounterexample.bpl.expect
new file mode 100644
index 000000000..3a76dd74f
--- /dev/null
+++ b/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

From 6540eeb23ff1976f4c3011498c68189292f8f231 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Tue, 28 Nov 2023 15:01:00 -0800
Subject: [PATCH 2/2] Bump version

---
 Source/Directory.Build.props | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
index 4304646ba..8a8ae0875 100644
--- a/Source/Directory.Build.props
+++ b/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>