Orienting for I_CONST_MERGE

2 files changed, 11 insertions, 8 deletions

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index b83b11608..9ea824f94 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -320,9 +320,10 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
               Node nrr = d_state.getRepresentative(n[count]);
               Assert(!d_eqcInfo[nrr].d_bestContent.isNull()
                      && d_eqcInfo[nrr].d_bestContent.isConst());
-              d_im.addToExplanation(n[count], d_eqcInfo[nrr].d_base, exp);
               // must flatten to avoid nested AND in explanations
               utils::flattenOp(AND,d_eqcInfo[nrr].d_exp,exp);
+              // now explain equality to base
+              d_im.addToExplanation(n[count], d_eqcInfo[nrr].d_base, exp);
             }
             else
             {
@@ -356,7 +357,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
               bei.d_exp = utils::mkAnd(exp);
             }
             Trace("strings-debug")
-                << "Set eqc best content " << n << " to " << nct << std::endl;
+                << "Set eqc best content " << n << " to " << nct << ", explanation = " << bei.d_exp << std::endl;
           }
         }
       }
@@ -371,11 +372,11 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
         BaseEqcInfo& bei = d_eqcInfo[nr];
         if (!bei.d_bestContent.isConst())
         {
-          Trace("strings-debug")
-              << "Set eqc const " << n << " to " << c << std::endl;
           bei.d_bestContent = c;
           bei.d_base = n;
           bei.d_exp = utils::mkAnd(exp);
+          Trace("strings-debug")
+              << "Set eqc const " << n << " to " << c << ", explanation = " << bei.d_exp << std::endl;
         }
         else if (c != bei.d_bestContent)
         {
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index d0f789a79..1396ae0db 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -90,10 +90,12 @@ void flattenOp(Kind k, Node n, std::vector<Node>& conj)
       visited.insert(cur);
       if (cur.getKind() == k)
       {
-        for (const Node& cn : cur)
-        {
-          visit.push_back(cn);
-        }
+        // Add in reverse order, so that we traverse left to right.
+        // This is important so that explantaions aren't reversed when they
+        // are flattened, which is important for proofs involving substitutions.
+        std::vector<Node> newChildren;
+        newChildren.insert(newChildren.end(),cur.begin(),cur.end());
+        visit.insert(visit.end(),newChildren.rbegin(),newChildren.rend());
       }
       else if (std::find(conj.begin(), conj.end(), cur) == conj.end())
       {