From cd91ef90ea461cd2d81ea69528c027f53f48b414 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 20 Jan 2022 18:42:51 -0600 Subject: [PATCH] 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. --- src/theory/strings/array_solver.cpp | 6 ++---- test/regress/regress0/seq/array/update-word-eq.smt2 | 1 - 2 files changed, 2 insertions(+), 5 deletions(-) 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 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) -- 2.30.2