Skip to content

Commit 9c758df

Browse files
committed
'--transform -b -e' fix: unfold correct rules in case they were shifted
1 parent 12a50bd commit 9c758df

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

metamath/DRuleParser.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2701,7 +2701,7 @@ vector<string> DRuleParser::recombineAbstractDProof(const vector<string>& abstra
27012701

27022702
// 5.3 Obtain unfolded proof.
27032703
vector<size_t> storedFundamentalLengths = measureFundamentalLengthsInAbstractDProof(indicesForNewProof, retractedDProof, abstractDProofConclusions, helperRules, helperRulesConclusions, debug, limit);
2704-
newAbstractDProof = unfoldRulesInAbstractDProof(indicesForNewProof, abstractDProof, helperRules, debug, &storedFundamentalLengths, storeIntermediateUnfoldingLimit);
2704+
newAbstractDProof = unfoldRulesInAbstractDProof(indicesForNewProof, retractedDProof, helperRules, debug, &storedFundamentalLengths, storeIntermediateUnfoldingLimit);
27052705
for (size_t i : indicesForNewProof) {
27062706
const shared_ptr<DlFormula>& f = i < retractedDProof.size() ? abstractDProofConclusions[i] : helperRulesConclusions[i - retractedDProof.size()];
27072707
out_conclusions.push_back(f);

0 commit comments

Comments
 (0)