Fix issues with cyclic proofs due to double SYMM applications (#7083)

Our way of constructing proofs from the equality engine in very rare cases may cause cyclic proofs due to constructing double applications of SYMM, which are not recognized as assumptions in CDProof. This is due to an interplay between LazyProofChain using an underlying CDProof as its default proof generator, where the proof chain would use the proofs from the CDProof to form a cyclic proof.

This was encountered in 9 SMT-LIB benchmarks in QF_SLIA.

This makes us safer in several places related to double SYMM steps.

1 files changed, 16 insertions, 7 deletions

diff --git a/src/proof/proof.cpp b/src/proof/proof.cpp
index 79f84135d..dc370a04d 100644
--- a/src/proof/proof.cpp
+++ b/src/proof/proof.cpp
@@ -97,8 +97,7 @@ std::shared_ptr<ProofNode> CDProof::getProofSymm(Node fact)
     if (pf == nullptr)
     {
       Trace("cdproof") << "...fresh make symm" << std::endl;
-      std::shared_ptr<ProofNode> psym =
-          d_manager->mkNode(PfRule::SYMM, pschild, args, fact);
+      std::shared_ptr<ProofNode> psym = d_manager->mkSymm(pfs, fact);
       Assert(psym != nullptr);
       d_nodes.insert(fact, psym);
       return psym;
@@ -411,13 +410,23 @@ bool CDProof::isAssumption(ProofNode* pn)
   {
     return true;
   }
-  else if (rule == PfRule::SYMM)
+  else if (rule != PfRule::SYMM)
   {
-    const std::vector<std::shared_ptr<ProofNode>>& pc = pn->getChildren();
-    Assert(pc.size() == 1);
-    return pc[0]->getRule() == PfRule::ASSUME;
+    return false;
   }
-  return false;
+  pn = ProofNodeManager::cancelDoubleSymm(pn);
+  rule = pn->getRule();
+  if (rule == PfRule::ASSUME)
+  {
+    return true;
+  }
+  else if (rule != PfRule::SYMM)
+  {
+    return false;
+  }
+  const std::vector<std::shared_ptr<ProofNode>>& pc = pn->getChildren();
+  Assert(pc.size() == 1);
+  return pc[0]->getRule() == PfRule::ASSUME;
 }
 
 bool CDProof::isSame(TNode f, TNode g)