transient

src/proof/alethe/alethe_post_processor.cpp

@@ -178,7 +178,8 @@ bool AletheProofPostprocessCallback::update(Node res,
     //======================== Assume and Scope
     case ProofRule::ASSUME:
     {
-      return addAletheStep(AletheRule::ASSUME, res, res, children, {}, *cdp);
+      return false;
+      // return addAletheStep(AletheRule::ASSUME, res, res, children, {}, *cdp);
     }
     // See proof_rule.h for documentation on the SCOPE rule. This comment uses
     // variable names as introduced there. Since the SCOPE rule originally
@@ -2394,16 +2395,17 @@ bool AletheProofPostprocessCallback::finalStep(Node res,
     children[0] = newChild;
   }
 
-  // Sanitize original assumptions and create a placeholder proof step to hold
-  // them.
-  Assert(id == ProofRule::SCOPE);
-  std::vector<Node> sanitizedArgs{
-      nm->mkConstInt(static_cast<uint32_t>(AletheRule::UNDEFINED)), res, res};
-  for (const Node& arg : args)
-  {
-    sanitizedArgs.push_back(d_anc.convert(arg, false));
-  }
-  return cdp->addStep(res, ProofRule::ALETHE_RULE, children, sanitizedArgs);
+  // Sanitize original assumptions and create a double scope to hold them, where
+  // the first scope is empty. This is needed because of the expected form a
+  // proof node to be printed
+  std::vector<Node> sanitizedArgs;
+  std::transform(args.begin(),
+                 args.end(),
+                 std::back_inserter(sanitizedArgs),
+                 [this](Node a) { return d_anc.convert(a, false); });
+  Node placeHolder = nm->mkNode(Kind::SEXPR, res);
+  cdp->addStep(placeHolder, ProofRule::SCOPE, children, sanitizedArgs);
+  return cdp->addStep(res, ProofRule::SCOPE, {placeHolder}, {});
 }
 
 bool AletheProofPostprocessCallback::addAletheStep(

src/proof/alf/alf_printer.cpp

@@ -274,6 +274,7 @@ void AlfPrinter::print(std::ostream& out, std::shared_ptr<ProofNode> pfn)
   Assert (pfn->getChildren()[0]->getRule()==ProofRule::SCOPE);
   const std::vector<Node>& assertions = pfn->getChildren()[0]->getArguments();
   const ProofNode* pnBody = pfn->getChildren()[0]->getChildren()[0].get();
+  Trace("test") << *pnBody << "\n";
 
   // Use a let binding if proofDagGlobal is true.
   // We can traverse binders due to the way we print global declare-var, since
@@ -488,7 +489,7 @@ void AlfPrinter::getArgsFromProofRule(const ProofNode* pn,
     }
     case ProofRule::ALETHE_RULE:
     {
-      Assert (args.size()>=3);
+      Assert (pargs.size()>=3) << *pn;
       // ignore the first argument, which specifies the rule and the second
       // argument which stores a conclusion
       args.insert(args.end(), pargs.begin()+3, pargs.end());