Skip to content

Commit

Permalink
Fix proof checker for quant var reodering (cvc5#11295)
Browse files Browse the repository at this point in the history
Fixes errors in nightlies.

This corrects the proof checker for QUANT_VAR_REORDERING, which
currently throws spurious errors due to an incorrect check.
  • Loading branch information
ajreynol authored Oct 21, 2024
1 parent 79b5507 commit 504fcaa
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/theory/quantifiers/proof_checker.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -137,8 +137,8 @@ Node QuantifiersProofRuleChecker::checkInternal(
std::unordered_set<Node> varSet1(eq[0][0].begin(), eq[0][0].end());
std::unordered_set<Node> varSet2(eq[1][0].begin(), eq[1][0].end());
// cannot have repetition
if (varSet1.size() != eq[0].getNumChildren()
|| varSet2.size() != eq[1].getNumChildren())
if (varSet1.size() != eq[0][0].getNumChildren()
|| varSet2.size() != eq[1][0].getNumChildren())
{
return Node::null();
}
Expand Down

0 comments on commit 504fcaa

Please sign in to comment.