Make verif. coverage work with -prune, renaming (#771)

Previously, enabling `-trackVerificationCoverage` along with either `-normalizeNames:1` or `-prune` would lead to malformed SMT queries. In particular, this made it not work with Dafny.
boogie-org · Aug 14, 2023 · 40f29df · 40f29df
1 parent eb7e2e5
commit 40f29df
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 4 deletions.
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -210,17 +210,22 @@ public override bool Visit(VCExprNAry node, bool arg)
       else if (node.Op is VCExprSoftOp)
       {
         var exprVar = node[0] as VCExprVar;
-        AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));
-        AddDeclaration(string.Format("(assert-soft {0} :weight {1})", exprVar.Name, ((VCExprSoftOp) node.Op).Weight));
+        string printedName = Namer.GetQuotedName(exprVar, exprVar.Name);
+        AddDeclaration(string.Format("(declare-fun {0} () Bool)", printedName));
+        AddDeclaration(string.Format("(assert-soft {0} :weight {1})", printedName, ((VCExprSoftOp) node.Op).Weight));
+        KnownVariables.Add(exprVar);
       }
       else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp) || node.Op.Equals(VCExpressionGenerator.NamedAssertOp))
       {
         var exprVar = node[0] as VCExprVar;
-        AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));
+        string printedName = Namer.GetQuotedName(exprVar, exprVar.Name);
+        AddDeclaration(string.Format("(declare-fun {0} () Bool)", printedName));
         if (options.TrackVerificationCoverage)
         {
-          AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name));
+          AddDeclaration(string.Format("(assert (! {0} :named {1}))", printedName, "aux$$" + exprVar.Name));
         }
+
+        KnownVariables.Add(exprVar);
       }
       else
       {

diff --git a/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl
@@ -2,6 +2,14 @@
 // RUN: %diff "%s.expect.plain" "%t.plain"
 // RUN: %boogie -trackVerificationCoverage "%s" > "%t.coverage"
 // RUN: %diff "%s.expect.coverage" "%t.coverage"
+// RUN: %boogie -trackVerificationCoverage -typeEncoding:a -prune "%s" > "%t.coverage-a"
+// RUN: %diff "%s.expect.coverage" "%t.coverage-a"
+// RUN: %boogie -trackVerificationCoverage -typeEncoding:p -prune "%s" > "%t.coverage-p"
+// RUN: %diff "%s.expect.coverage" "%t.coverage-p"
+// RUN: %boogie -trackVerificationCoverage -normalizeDeclarationOrder:1 -prune "%s" > "%t.coverage-d"
+// RUN: %diff "%s.expect.coverage" "%t.coverage-d"
+// RUN %boogie -trackVerificationCoverage -normalizeNames:1 -prune "%s" > "%t.coverage-n"
+// RUN %diff "%s.expect.coverage" "%t.coverage-n"
 // UNSUPPORTED: batch_mode
 
 procedure testRequiresAssign(n: int)