From 22b0ff77781b957c3ed714dd7ac88fb8c5a8d25c Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 28 Oct 2021 15:59:43 -0300
Subject: [PATCH] [proofs] Fix assertion in EqProof conversion  (#7522)

Also improves a few traces.

Fixes cvc5/cvc5-projects#330
---
 src/theory/uf/eq_proof.cpp                            | 11 ++++++++---
 test/regress/CMakeLists.txt                           |  1 +
 .../regress0/proofs/project-issue330-eqproof.smt2     |  7 +++++++
 3 files changed, 16 insertions(+), 3 deletions(-)
 create mode 100644 test/regress/regress0/proofs/project-issue330-eqproof.smt2

diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 45a00a620..ab091cffd 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -91,8 +91,8 @@ void EqProof::cleanReflPremises(std::vector<Node>& premises) const
   if (newPremises.size() != size)
   {
     Trace("eqproof-conv") << "EqProof::cleanReflPremises: removed "
-                          << (newPremises.size() >= size
-                                  ? newPremises.size() - size
+                          << (size >= newPremises.size()
+                                  ? size - newPremises.size()
                                   : 0)
                           << " refl premises from " << premises << "\n";
     premises.clear();
@@ -138,6 +138,8 @@ bool EqProof::expandTransitivityForDisequalities(
   // if no equality of the searched form, nothing to do
   if (offending == size)
   {
+    Trace("eqproof-conv")
+        << "EqProof::expandTransitivityForDisequalities: no need.\n";
     return false;
   }
   NodeManager* nm = NodeManager::currentNM();
@@ -967,6 +969,7 @@ Node EqProof::addToProof(CDProof* p,
   if (d_id == MERGED_THROUGH_REFLEXIVITY
       || (d_node.getKind() == kind::EQUAL && d_node[0] == d_node[1]))
   {
+    Trace("eqproof-conv") << "EqProof::addToProof: refl step\n";
     Node conclusion =
         d_node.getKind() == kind::EQUAL ? d_node : d_node.eqNode(d_node);
     p->addStep(conclusion, PfRule::REFL, {}, {conclusion[0]});
@@ -1170,7 +1173,9 @@ Node EqProof::addToProof(CDProof* p,
         }
       }
     }
-    Assert(p->hasStep(conclusion));
+    Assert(p->hasStep(conclusion) || assumptions.count(conclusion))
+        << "Conclusion " << conclusion
+        << " does not have a step in the proof neither it's an assumption.\n";
     visited[d_node] = conclusion;
     return conclusion;
   }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2529a8622..2430eb13f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -864,6 +864,7 @@ set(regress_0_tests
   regress0/proofs/open-pf-if-unordered-iff.smt2
   regress0/proofs/open-pf-rederivation.smt2
   regress0/proofs/project-issue317-inc-sat-conflictlit.smt2
+  regress0/proofs/project-issue330-eqproof.smt2
   regress0/proofs/qgu-fuzz-1-bool-sat.smt2
   regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2
   regress0/proofs/qgu-fuzz-3-chainres-checking.smt2
diff --git a/test/regress/regress0/proofs/project-issue330-eqproof.smt2 b/test/regress/regress0/proofs/project-issue330-eqproof.smt2
new file mode 100644
index 000000000..1da778205
--- /dev/null
+++ b/test/regress/regress0/proofs/project-issue330-eqproof.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+(set-logic QF_SLIA)
+(declare-const x String)
+(declare-const x1 Int)
+(set-option :check-proofs true)
+(declare-const _x String)
+(check-sat-assuming ((>= 0 (ite (= x (str.++ (str.from_code 0) (str.replace_all x (str.from_code 0) (str.++ (str.from_code 0) (str.from_code 0))) _x) (ite false x (str.++ _x _x _x)) x) x1 0))))
\ No newline at end of file
-- 
2.30.2