Make verif. coverage work with -prune, renaming

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.

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
       {

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)