From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 21 Jan 2022 00:42:51 +0000 (-0600)
Subject: Fix trivial explantions in sequences array solver (#7973)
X-Git-Tag: cvc5-1.0.0~519
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cd91ef90ea461cd2d81ea69528c027f53f48b414;p=cvc5.git

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 3d364bf3c..a4ac38d03 100644
--- 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 98c037383..f81077c6f 100644
--- 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)