Fix trivial explantions in sequences array solver (#7973)

Also tightens the explanation slightly, we were previously adding a spurious equality to the representative, instead of the base of the normal form.

diff --git a/src/theory/strings/array_solver.cpp b/src/theory/strings/array_solver.cpp
index 3d364bf3ca06396225bf424afe2f774f60e87b2e..a4ac38d03f464848397562f861b410651226851c 100644 (file)
--- a/src/theory/strings/array_solver.cpp
+++ b/src/theory/strings/array_solver.cpp
@@ -373,16 +373,14 @@ void ArraySolver::checkTerm(Node t, bool checkInv)
   std::vector<Node> exp;
   if (checkInv)
   {
-    d_im.addToExplanation(rself, t, exp);
     NormalForm& nfSelf = d_csolver.getNormalForm(rself);
     exp.insert(exp.end(), nfSelf.d_exp.begin(), nfSelf.d_exp.end());
-    exp.push_back(t.eqNode(nfSelf.d_base));
+    d_im.addToExplanation(t, nfSelf.d_base, exp);
   }
   else
   {
-    d_im.addToExplanation(r, t[0], exp);
     exp.insert(exp.end(), nf.d_exp.begin(), nf.d_exp.end());
-    exp.push_back(t[0].eqNode(nf.d_base));
+    d_im.addToExplanation(t[0], nf.d_base, exp);
   }
   if (d_eqProc.find(eq) == d_eqProc.end())
   {

diff --git a/test/regress/regress0/seq/array/update-word-eq.smt2 b/test/regress/regress0/seq/array/update-word-eq.smt2
index 98c0373831b21785f0bdb22a3bc8e617bf9835b8..f81077c6fb47ef54d48da39f8aa0274d25b2512a 100644 (file)
--- a/test/regress/regress0/seq/array/update-word-eq.smt2
+++ b/test/regress/regress0/seq/array/update-word-eq.smt2
@@ -1,5 +1,4 @@
 ; COMMAND-LINE: --strings-exp --seq-array=eager
-; DISABLE-TESTER: proof
 (set-logic QF_SLIA)
 (set-info :status unsat)