Extended rewriter to show core steps in strings reconstruction

1 files changed, 5 insertions, 1 deletions

diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 8812c971a..61fa6116f 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -259,8 +259,12 @@ void InferProofCons::convert(InferenceId infer,
       childrenSRew.push_back(pmainEq);
       childrenSRew.insert(childrenSRew.end(), pcsr.begin(), pcsr.end());
       // now, conclude the proper equality
+      std::vector<Node> argsSRew;
+      addMethodIds(argsSRew, MethodId::SB_DEFAULT,
+                                   MethodId::SBA_SEQUENTIAL,
+                                   MethodId::RW_EXT_REWRITE);
       Node mainEqSRew =
-          psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, {});
+          psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, argsSRew);
       if (CDProof::isSame(mainEqSRew, pmainEq))
       {
         Trace("strings-ipc-core") << "...undo step" << std::endl;