fix prefixing of identifiers in subproofs

HanielB · Feb 29, 2024 · da005bf · da005bf
1 parent 4cd8d6d
commit da005bf
Showing 1 changed file with 1 addition and 3 deletions.
diff --git a/src/proof/alethe/alethe_printer.cpp b/src/proof/alethe/alethe_printer.cpp
@@ -223,8 +223,7 @@ void AletheProofPrinter::printInternal(
     Trace("alethe-printer") << push;
     Assert(pfChildren.size() == 1);
     out << "(anchor :step " << prefix << "t" << id;
-    std::string subproofPrefix =
-        prefix + (prefix == "" ? "" : ".") + "t" + std::to_string(id) + ".";
+    std::string subproofPrefix = prefix + "t" + std::to_string(id) + ".";
     std::unordered_map<Node, std::string> subproofAssumptionsMap{assumptionsMap.begin(), assumptionsMap.end()};
     std::unordered_map<std::shared_ptr<ProofNode>, std::string> subproofPfMap{pfMap.begin(), pfMap.end()};
     // since the subproof shape relies on having at least one step inside it, if
@@ -235,7 +234,6 @@ void AletheProofPrinter::printInternal(
     {
       subproofPfMap.erase(it);
     }
-
     // if subproof, print assumptions, other print arguments
     if (arule == AletheRule::ANCHOR_SUBPROOF)
     {