diff --git a/ChangeLog b/ChangeLog
index 113fad67..b5f8b25c 100755
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,13 @@
+2023-05-05  Steven Eker  <eker@pup>
+
+	* tests/ResolvedBugs/stripperCollectorSwitchMay2023.maude: added
+
+2023-05-03  Steven Eker  <eker@pup>
+
+	* tests/Corner/ACU_TreeVariableSubproblem.maude: added
+
+==================================Maude148===========================================
+
 2023-04-28  Steven Eker  <eker@pup>
 
 	* tests/ResolvedBugs/redBlackNGA_April2023.maude: added
diff --git a/NEWS b/NEWS
index c951d563..c46ef6d1 100755
--- a/NEWS
+++ b/NEWS
@@ -1,4 +1,18 @@
-Overview of Changes in alpha147
+Overview of Changes in alpha148 (2023-05-05)
+============================================
+* fixed a bug in compilation of ACU patterns introduced by the
+last alpha that caused matches to be missed
+* fixed a bug in thew functional meta-level where rewrite count
+from metaSrewrite() was lost
+* more optimizations for ACU red-black matching
+* smarter scheme for deciding how many dagnodes the memory manager
+should allocate
+* fixed a bug in the rewrite count values returned by the
+meta-interpeter in response to the srewriteTerm() message
+* more information shown in garbage collection reporting
+* -early-quit=N flag for developer use
+
+Overview of Changes in alpha147 (2023-04-28)
 ============================================
 * fixed bug in new ACU matching code where stripper variable
 was not required to have multiplicity 1
@@ -6,7 +20,7 @@ was not required to have multiplicity 1
 0 or 1 subject arguments left
 * fixed bug in new ACU matching code where it could be used
 even if a non-ground alien was present
-* optimizatons for ACU red-black matching
+* optimizations for ACU red-black matching
 
 Overview of Changes in alpha146 (2023-04-26)
 ============================================
diff --git a/configure b/configure
index 379447ad..56ecb774 100755
--- a/configure
+++ b/configure
@@ -1,6 +1,6 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.69 for Maude alpha147.
+# Generated by GNU Autoconf 2.69 for Maude alpha148.
 #
 # Report bugs to <maude-bugs@lists.cs.illinois.edu>.
 #
@@ -580,8 +580,8 @@ MAKEFLAGS=
 # Identity of this package.
 PACKAGE_NAME='Maude'
 PACKAGE_TARNAME='maude'
-PACKAGE_VERSION='alpha147'
-PACKAGE_STRING='Maude alpha147'
+PACKAGE_VERSION='alpha148'
+PACKAGE_STRING='Maude alpha148'
 PACKAGE_BUGREPORT='maude-bugs@lists.cs.illinois.edu'
 PACKAGE_URL=''
 
@@ -1312,7 +1312,7 @@ if test "$ac_init_help" = "long"; then
   # Omit some internal or obsolete options to make the list less imposing.
   # This message is too long to be a string in the A/UX 3.1 sh.
   cat <<_ACEOF
-\`configure' configures Maude alpha147 to adapt to many kinds of systems.
+\`configure' configures Maude alpha148 to adapt to many kinds of systems.
 
 Usage: $0 [OPTION]... [VAR=VALUE]...
 
@@ -1383,7 +1383,7 @@ fi
 
 if test -n "$ac_init_help"; then
   case $ac_init_help in
-     short | recursive ) echo "Configuration of Maude alpha147:";;
+     short | recursive ) echo "Configuration of Maude alpha148:";;
    esac
   cat <<\_ACEOF
 
@@ -1490,7 +1490,7 @@ fi
 test -n "$ac_init_help" && exit $ac_status
 if $ac_init_version; then
   cat <<\_ACEOF
-Maude configure alpha147
+Maude configure alpha148
 generated by GNU Autoconf 2.69
 
 Copyright (C) 2012 Free Software Foundation, Inc.
@@ -2013,7 +2013,7 @@ cat >config.log <<_ACEOF
 This file contains any messages produced by compilers while
 running configure, to aid debugging if configure makes a mistake.
 
-It was created by Maude $as_me alpha147, which was
+It was created by Maude $as_me alpha148, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   $ $0 $@
@@ -2962,7 +2962,7 @@ fi
 
 # Define the identity of the package.
  PACKAGE='maude'
- VERSION='alpha147'
+ VERSION='alpha148'
 
 
 cat >>confdefs.h <<_ACEOF
@@ -6623,7 +6623,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1
 # report actual input values of CONFIG_FILES etc. instead of their
 # values after options handling.
 ac_log="
-This file was extended by Maude $as_me alpha147, which was
+This file was extended by Maude $as_me alpha148, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
@@ -6689,7 +6689,7 @@ _ACEOF
 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`"
 ac_cs_version="\\
-Maude config.status alpha147
+Maude config.status alpha148
 configured by $0, generated by GNU Autoconf 2.69,
   with options \\"\$ac_cs_config\\"
 
diff --git a/configure.ac b/configure.ac
index 0578c9c8..f5025f9c 100755
--- a/configure.ac
+++ b/configure.ac
@@ -3,7 +3,7 @@
 #
 #	Initialize autoconf stuff.
 #
-AC_INIT(Maude, alpha147, [maude-bugs@lists.cs.illinois.edu])
+AC_INIT(Maude, alpha148, [maude-bugs@lists.cs.illinois.edu])
 #
 #	Allow directory names that look like macros.
 #
diff --git a/doc/Makefile.am b/doc/Makefile.am
index d10b6243..8b0eb16b 100644
--- a/doc/Makefile.am
+++ b/doc/Makefile.am
@@ -15,4 +15,5 @@ EXTRA_DIST = \
 	alpha144.txt \
 	alpha145.txt \
 	alpha146.txt \
-	alpha147.txt
+	alpha147.txt \
+	alpha148.txt
diff --git a/doc/Makefile.in b/doc/Makefile.in
index 269ec147..8e9d4bec 100644
--- a/doc/Makefile.in
+++ b/doc/Makefile.in
@@ -247,7 +247,8 @@ EXTRA_DIST = \
 	alpha144.txt \
 	alpha145.txt \
 	alpha146.txt \
-	alpha147.txt
+	alpha147.txt \
+	alpha148.txt
 
 all: all-am
 
diff --git a/doc/alpha148.txt b/doc/alpha148.txt
new file mode 100644
index 00000000..7c104d6a
--- /dev/null
+++ b/doc/alpha148.txt
@@ -0,0 +1,86 @@
+Alpha 148 release notes
+========================
+
+Bug fixes
+==========
+
+(1) A bug in the new ACU matching code where the variables were sorted
+after the indices for ths stripper and collector variables for AC/ACU
+red-black matching had been stored, during compilation, invalidating them
+and causing missed matches. It's quite a tricky bug to demonstrate
+because the variables are also sorted before compilation as part of theory
+normalization.
+
+fmod FOO is
+  pr NAT .
+  sorts Set Elt .
+  subsort Elt < Set .
+var S : Set .
+var E : Elt .
+var N : Nat .
+  op dummy : Set -> Set .
+  eq dummy(S) = S .  *** needed to influence AC ordering
+
+  op z : -> Elt .
+  op p_ : Elt -> Elt .
+  op g : Nat Set -> Set .
+  eq g(s N, E) = f(g(N, p E), E) .
+  
+  op f : Set Set -> Set [assoc comm] .
+  op h : Set -> Bool .
+  ceq h(f(S, E)) = true if E = z .
+endfm
+
+red h(g(7, z)) .  *** OK because argument list is too short to be red-black
+red h(g(8, z)) .  *** fails
+
+(2) A bug in the functional metalevel where metaSrewrite() did not
+transfer the rewrite count from the meta-operation to the top level
+context. Illustrated by this example from the test suite:
+
+red in META-LEVEL : metaSrewrite(
+mod 'INC is
+  protecting 'NAT .
+  sorts none .
+  none
+  none
+  none
+  none
+  rl 'N:Nat => 's_['N:Nat] [label('inc)] .
+endm, '0.Nat, ('inc[none]{empty}) *, breadthFirst, 8) .
+
+(3) A bug in the meta-interpreter where the rewrite count from the
+meta-computations performed on behalf of the srewriteTerm() message would
+only be transferred to the enclosing context if and when failure was seen.
+This resulting in the wrong number of rewrites being returned in
+srewroteTerm() messages other than the first, and in the noSuchResult()
+message. Also those rewrites were missing from the top level total if
+the computation did not proceed far enough that the noSuchResult() message
+was seen
+
+Other changes
+==============
+
+(1) ACU matching subproblems in the stripper-collector case when all
+solutions are required no longer caches solutions as it seems to be a net
+lose.
+
+(2) Fast handling for ACU matching subproblems in the stripper-collector
+case where the stripper and/or collector variable is already bound.
+
+(3) A smarter scheme for deciding when to allocate more dag nodes. This idea
+came from the observation that while not caching solutions in (1) saved
+time and memory for matching, it made the system slower overall because
+fewer dag nodes were needed and thus garbage collections were needed more
+frequently. 
+
+(4) If garbage collection reporting is turned on with
+  set show gc on .
+the number of the garbage collection is now shown and the other information
+is also given in megabytes.
+
+(5) There is a command line flag
+  -early-quit=N
+which causes Maude to quit abruptly after the Nth garbage collection. This
+is intended for developer use only, to assist in profiling long running
+examples.
diff --git a/src/ACU_Persistent/ACU_SlowIter.hh b/src/ACU_Persistent/ACU_SlowIter.hh
index 40e3e84b..d156809c 100644
--- a/src/ACU_Persistent/ACU_SlowIter.hh
+++ b/src/ACU_Persistent/ACU_SlowIter.hh
@@ -2,7 +2,7 @@
 
     This file is part of the Maude 3 interpreter.
 
-    Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
+    Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA.
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -38,7 +38,8 @@ class ACU_SlowIter : public ACU_Stack
 public:
   ACU_SlowIter();
   ACU_SlowIter(const ACU_Tree& tree);
-  
+  void reset(const ACU_Tree& tree);  // so we can reuse an existing ACU_SlowIter
+
   bool valid() const;
   DagNode* getDagNode() const;
   int getMultiplicity() const;
@@ -56,6 +57,13 @@ ACU_SlowIter::ACU_SlowIter(const ACU_Tree& tree)
   stackLeftmostPath(tree.root);
 }
 
+inline void
+ACU_SlowIter::reset(const ACU_Tree& tree)
+{
+  clear();
+  stackLeftmostPath(tree.root);
+}
+
 inline bool
 ACU_SlowIter::valid() const
 {
diff --git a/src/ACU_Persistent/ChangeLog b/src/ACU_Persistent/ChangeLog
index cdc0e659..fd65b67e 100755
--- a/src/ACU_Persistent/ChangeLog
+++ b/src/ACU_Persistent/ChangeLog
@@ -1,3 +1,9 @@
+2023-05-02  Steven Eker  <eker@pup>
+
+	* ACU_SlowIter.hh (ACU_SlowIter::reset): added
+
+===================================Maude148===========================================
+
 2019-07-01  Steven Eker  <eker@mu>
 
 	* ACU_RedBlackNode.hh: rewritten using new MemoryCell definition
diff --git a/src/ACU_Theory/ACU_LhsAutomaton.cc b/src/ACU_Theory/ACU_LhsAutomaton.cc
index e9dff595..36365c28 100644
--- a/src/ACU_Theory/ACU_LhsAutomaton.cc
+++ b/src/ACU_Theory/ACU_LhsAutomaton.cc
@@ -131,25 +131,11 @@ ACU_LhsAutomaton::addTopVariable(const VariableTerm* variable,
 				 int multiplicity,
 				 bool willBeBound)
 {
-  int nrTopVariables = topVariables.length();
   Sort* s = variable->getSort();
   int bound = topSymbol->sortBound(s);
   bool takeIdentity = topSymbol->takeIdentity(s);
-  if (!willBeBound)
-    {
-      //
-      //	We don't expect the variable to be bound at match time before doing
-      //	a match with this automaton.
-      //
-      ++nrExpectedUnboundVariables;
-      if (multiplicity == 1)
-	{
-	  if (stripperIndex == NONE && !takeIdentity && bound == 1)
-	    stripperIndex = nrTopVariables;
-	  else if (collectorIndex == NONE && bound == UNBOUNDED)
-	    collectorIndex = nrTopVariables;
-	}
-    }
+
+  int nrTopVariables = topVariables.length();
   topVariables.expandBy(1);
   TopVariable& tv = topVariables[nrTopVariables];
   tv.index = variable->getIndex();
@@ -157,8 +143,10 @@ ACU_LhsAutomaton::addTopVariable(const VariableTerm* variable,
   tv.sort = s;
   tv.upperBound = bound;
   tv.structure = topSymbol->sortStructure(s);
-  tv.takeIdentity = takeIdentity;
   tv.abstracted = 0;
+  tv.takeIdentity = takeIdentity;
+  tv.willBeBound = willBeBound;
+
   updateTotals(takeIdentity ? 0 : multiplicity,
 	       (bound == UNBOUNDED) ? UNBOUNDED : (bound * multiplicity));
 }
@@ -237,6 +225,10 @@ void
 ACU_LhsAutomaton::complete(MatchStrategy strategy,
 			   int nrIndependent)
 {
+  //
+  //	We need to sort variables before storing indices to variables.
+  //
+  sort(topVariables.begin(), topVariables.end(), topVariableLt);
   //
   //	For red-black greedy matching to be correct we require that
   //	(1) unbound top variables are quasi-linear and don't occur in the
@@ -260,6 +252,26 @@ ACU_LhsAutomaton::complete(MatchStrategy strategy,
   //
   if (treeMatchOK)
     {
+      Index nrVariables = topVariables.size();
+      for (Index i = 0; i < nrVariables; ++i)
+	{
+	  const TopVariable& tv = topVariables[i];
+	  if (!tv.willBeBound)
+	    {
+	      //
+	      //	We don't expect the variable to be bound at match time before doing
+	      //	a match with this automaton.
+	      //
+	      ++nrExpectedUnboundVariables;
+	      if (tv.multiplicity == 1)
+		{
+		  if (stripperIndex == NONE && !tv.takeIdentity && tv.upperBound == 1)
+		    stripperIndex = i;
+		  else if (collectorIndex == NONE && tv.upperBound == UNBOUNDED)
+		    collectorIndex = i;
+		}
+	    }
+	}
       if (strategy == LONE_VARIABLE || strategy == GREEDY)
 	treeMatchOK = collectorIndex != NONE || matchAtTop;
       else if (strategy == FULL)
@@ -286,11 +298,9 @@ ACU_LhsAutomaton::complete(MatchStrategy strategy,
       else
 	treeMatchOK = false;
     }
-
   matchStrategy = strategy;
   Assert(nrIndependent <= nonGroundAliens.length(), "too many independent");
   nrIndependentAliens = nrIndependent;
-  sort(topVariables.begin(), topVariables.end(), topVariableLt);
 }
 
 #ifdef DUMP
diff --git a/src/ACU_Theory/ACU_LhsAutomaton.hh b/src/ACU_Theory/ACU_LhsAutomaton.hh
index 7d6b6693..8aaf00b8 100644
--- a/src/ACU_Theory/ACU_LhsAutomaton.hh
+++ b/src/ACU_Theory/ACU_LhsAutomaton.hh
@@ -132,8 +132,9 @@ private:
     Sort* sort;
     int upperBound;
     AssociativeSymbol::Structure structure;
-    bool takeIdentity;
     LhsAutomaton* abstracted;	// automaton for abstracted term
+    bool takeIdentity;
+    bool willBeBound;  // will be bound at match time
     //
     //	Data storage for match-time use
     //
@@ -260,7 +261,7 @@ private:
   int maxPatternMultiplicity;  // must have at least on subject with >= this multiplicity
   int totalNonGroundAliensMultiplicity;
   int nrIndependentAliens;
-  int nrExpectedUnboundVariables;  // used at semicompile time only
+  int nrExpectedUnboundVariables;  // used at semicompile time only, for red-black case only
   LhsAutomaton* uniqueCollapseAutomaton;
   Vector<TopVariable> topVariables;
   Vector<GroundAlien> groundAliens;
diff --git a/src/ACU_Theory/ACU_TreeMatcher.cc b/src/ACU_Theory/ACU_TreeMatcher.cc
index 7543d463..6a8b5544 100644
--- a/src/ACU_Theory/ACU_TreeMatcher.cc
+++ b/src/ACU_Theory/ACU_TreeMatcher.cc
@@ -39,6 +39,7 @@ ACU_LhsAutomaton::eliminateBoundVariables(Substitution& solution)
 	      //	Variable was bound to a term with our top symbol.
 	      //	This needs more complicated handling that is unlikely to be efficient with a red-black tree.
 	      //
+	      Profile(RED, "T");
 	      return UNDECIDED;
 	    }
 	  if (identity == nullptr || !(identity->equal(d)))  // we can ignore variables bound to our identity
@@ -147,10 +148,13 @@ ACU_LhsAutomaton::treeMatch(ACU_TreeDagNode* subject,
   //
   if (extensionInfo == nullptr && nonGroundAliens.empty())
     {
+      //
+      //	No extension and only variables left.
+      //
       if (nrUnboundVariables == 0)
 	{
 	  //
-	  //	Everything in the pattern has had a forced match and no extension.
+	  //	Everything in the pattern had a unique match and no extension.
 	  //	We succeed iff there are no subject arguments left.
 	  //
 	  return current.getSize() == 0;
diff --git a/src/ACU_Theory/ACU_TreeVariableSubproblem.cc b/src/ACU_Theory/ACU_TreeVariableSubproblem.cc
index ece264fa..a5b364bf 100644
--- a/src/ACU_Theory/ACU_TreeVariableSubproblem.cc
+++ b/src/ACU_Theory/ACU_TreeVariableSubproblem.cc
@@ -47,13 +47,14 @@
 #include "substitution.hh"
 #include "rewritingContext.hh"
 #include "localBinding.hh"
+#include "dagArgumentIterator.hh"
 
 //	ACU theory class definitions
 #include "ACU_Symbol.hh"
 #include "ACU_TreeDagNode.hh"
 #include "ACU_TreeVariableSubproblem.hh"
 
-ACU_TreeVariableSubproblem::ACU_TreeVariableSubproblem(ACU_BaseDagNode* subject,
+ACU_TreeVariableSubproblem::ACU_TreeVariableSubproblem(const ACU_TreeDagNode* subject,
 						       const ACU_Tree& remaining,
 						       int stripperVarIndex,
 						       Sort* stripperSort,
@@ -64,17 +65,10 @@ ACU_TreeVariableSubproblem::ACU_TreeVariableSubproblem(ACU_BaseDagNode* subject,
     stripperVarIndex(stripperVarIndex),
     stripperSort(stripperSort),
     collectorVarIndex(collectorVarIndex),
-    collectorSort(collectorSort),
-    currentPath(remaining)
+    collectorSort(collectorSort)
 {
-  previous.reserve(remaining.getSize());
-  previousIndex = NONE;
-}
-
-ACU_TreeVariableSubproblem::~ACU_TreeVariableSubproblem()
-{
-  for (LocalBinding* i : previous)
-    delete i;
+  Assert(remaining.getSize() != 0, "no remaining subject arguments");
+  Assert(remaining.getSize() > 1 || remaining.getMaxMult() > 1, "only one subject argument remaining");
 }
 
 bool
@@ -83,105 +77,285 @@ ACU_TreeVariableSubproblem::solve(bool findFirst, RewritingContext& solution)
   if (findFirst)
     {
       //
-      //	We're asked to find the first match with current global solution.
-      //	This doens't mean that we haven't found and saved local matches
-      //	before, on behalf of a previous global solution.
+      //	Record state of stripper and collector variables on entry so we can restore
+      //	them on backtracking.
+      //
+      stripperAlreadyBound = (solution.value(stripperVarIndex) != nullptr);
+      collectorAlreadyBound = (solution.value(collectorVarIndex) != nullptr);
+      if (collectorAlreadyBound)
+	{
+	  //
+	  //	Having the collector variable bound, whether or not the stripper variable
+	  //	is bound is an unusual situation. It must have been bound by a sub-match
+	  //	after the sub-match that created this problem, or by a subproblem
+	  //	created for a sub-match before the sub-match that created this problem.
+	  //	There can be at most one solution.
+	  //
+	  return handleBoundCollector(solution);
+	}
+      if (stripperAlreadyBound)
+	{
+	  //
+	  //	The stripper variable can be bound by the same means as described above.
+	  //	For some reason this is quite a common occurrence, and we need to handle
+	  //	it efficiently. There can be at most one solution.
+	  //
+	  return handleBoundStripper(solution);
+	}
+      //
+      //	Stripper and collect are both free - start a systematic search for subject arguments
+      //	to bind stripper variable to.
       //
-      if (previousIndex != NONE && previous.empty())
-	return false;  // there were no local matches
-      previousIndex = 0;
+      currentPath.reset(remaining);
     }
   else
     {
       //
-      //	Undo last solution.
+      //	Restore solution to state before last solve() by clearing any bindings we created.
       //
-      previous[previousIndex]->retract(solution);
-      ++previousIndex;
+      if (!stripperAlreadyBound)
+	solution.bind(stripperVarIndex, nullptr);
+      if (!collectorAlreadyBound)
+	solution.bind(collectorVarIndex, nullptr);
+      //
+      //	If either variable was bound before we found a first solution, this implies the
+      //	solution was unique.
+      //
+      if (stripperAlreadyBound || collectorAlreadyBound)
+	return false;
     }
   //
-  //	Try the next previously generated match.
   //
-  int nrPrevious = previous.size();
-  for (; previousIndex < nrPrevious; ++previousIndex)
+  //	Try next alternative for the stripper variable.
+  //
+  for (; currentPath.valid(); currentPath.next())
+    {
+      DagNode* sVal = currentPath.getDagNode();
+      if (leq(sVal->getSortIndex(), stripperSort) && bindCollector(solution))  // can't update currentPath before bindCollector()
+	{
+	  //
+	  //	Got a match.
+	  //
+	  solution.bind(stripperVarIndex, sVal);
+	  currentPath.next();  // must always move to the next alternative
+	  return true;
+	}
+    }
+  return false;
+}
+
+bool
+ACU_TreeVariableSubproblem::handleBoundCollector(RewritingContext& solution)
+{
+  DagNode* cVal = solution.value(collectorVarIndex);
+  Term* identity = subject->symbol()->getIdentity();
+  if (identity != nullptr && identity->equal(cVal))
     {
-      if (previous[previousIndex]->assert(solution))
-	return true;
+      //
+      //	We have at least 2 subject arguments remaining and the stripper variable can take at most 1
+      //	so if the collector takes the identity, no match is possible.
+      //
+      return false;
     }
   //
-  //	Try to generate new matches; this will usually be on behalf of the
-  //	first global solution, but it is legal to start with findFirst = true
-  //	with a new global solution, even if the we didn't exhaust matches
-  //	for the previous global solution.
+  //	We need exactly one argument left over from remaining after cVal is subtracted.
   //
-  for (; currentPath.valid(); currentPath.next())
+  DagNode* leftOver = nullptr;
+ 
+  if (cVal->symbol() == subject->symbol())
     {
       //
-      //	We general local bindings directly; we potentially need all of
-      //	them regardless of whether they are compatible with the current
-      //	global solution we were given.
+      //	Collector variable is bound to a term headed by the same ACU symbol.
+      //	It could be in tree or argVec form so we use a slow general purpose iterator
+      //	to inspect its arguments.
       //
+      currentPath.reset(remaining);
+      Assert(currentPath.valid(), "no remaining arguments");
       DagNode* d = currentPath.getDagNode();
-      if (leq(d->getSortIndex(), stripperSort))
+      int multiplicity = currentPath.getMultiplicity();
+      for (DagArgumentIterator i(cVal); i.valid(); i.next())
 	{
-	  if (DagNode* c = collect(solution))
+	  DagNode* c = i.argument();
+	  //
+	  //	Try count off 1 copy of c.
+	  //
+	  for (;;)
 	    {
-	      LocalBinding* b = new LocalBinding(2);
-	      b->addBinding(stripperVarIndex, d);
-	      b->addBinding(collectorVarIndex, c);
-	      previous.push_back(b);
-	      if (b->assert(solution))
+	      if (c->equal(d))
 		{
-		  currentPath.next();  // must not try the same argument again
-		  return true;
+		  if (multiplicity == 0)
+		    return false;  // multiplicity exhausted
+		  --multiplicity;
+		  break;
 		}
+	      else
+		{
+		  //
+		  //	Deal with left over multiplicity of d.
+		  //
+		  if (multiplicity > 1)
+		    return false;  // more than copy of d left over
+		  if (multiplicity == 1)
+		    {
+		      if (leftOver != nullptr)
+			return false;  // leftOver already full
+		      leftOver = d;
+		    }
+		  //
+		  //	Move to next remaining argument to try and find c.
+		  //
+		  currentPath.next();
+		  if (!currentPath.valid())
+		    return false;  // no more remaining arguments
+		  d = currentPath.getDagNode();
+		  multiplicity = currentPath.getMultiplicity();
+		}
+	    }
+	}
+      //
+      //	We have now seen everything in cVal. Need to check what is left for stripper variable.
+      //
+      if (leftOver == nullptr)
+	{
+	  if (multiplicity > 1)
+	    return false;  // too much
+	  if (multiplicity == 1)
+	    leftOver = d;  // just right
+	  else
+	    {
+	      currentPath.next();
+	      if (!currentPath.valid() || currentPath.getMultiplicity() > 1)
+		return false;  // nothing or too much
+	      leftOver = currentPath.getDagNode();  // just right
 	    }
 	}
+      else if (multiplicity > 0)
+	return false;  // leftOver already full
+      //
+      //	We have a dagNode for stripper variable.
+      //	Need to check if there in anything left in remaining.
+      //
+      currentPath.next();
+      if (currentPath.valid())
+	return false; // leftOver already full
+    }
+  else
+    {
+      //
+      //	Collector variable is bound to an alien.
+      //	We check that this alien appears in remaining and there is only one other argument left.
+      //	We are going to examine at most 2 arguments of remaining so we don't bother with find().
+      //
+      for (currentPath.reset(remaining); currentPath.valid(); currentPath.next())
+	{
+	  DagNode* d = currentPath.getDagNode();
+	  int multiplicity = currentPath.getMultiplicity();
+	  if (d->equal(cVal))
+	    {
+	      if (multiplicity > 2)
+		return false;  // stripper can take only one copy
+	      if (multiplicity == 2)
+		{
+		  if (leftOver != nullptr)
+		    return false;
+		  leftOver = d;
+		}
+	    }
+	  else
+	    {
+	      if (leftOver != nullptr || multiplicity > 1)
+		return false;  // stripper can take only one argument
+	      leftOver = d;
+	    }
+	}
+      //
+      //	Because we have at least two arguments remaining, if we haven't returned false,
+      //	then it is because we had exactly two arguments remaining, at least one of them
+      //	is equal to cVal and leftOver points to the other (which could be equal to cVal also).
+      //
+      Assert(leftOver != nullptr, "nothing left over with collector = " << cVal);
+    }
+  //
+  //	We've seen cVal and there is one argument left over; check whether it agrees with
+  //	or can be assigned to stripper variable.
+  //
+  DagNode* sVal = solution.value(stripperVarIndex);
+  if (sVal != nullptr)
+    return sVal->equal(leftOver);
+  if (leq(leftOver->getSortIndex(), stripperSort))
+    {
+      solution.bind(stripperVarIndex, leftOver);
+      return true;
     }
   return false;
 }
 
-DagNode*
-ACU_TreeVariableSubproblem::collect(RewritingContext& solution)
+bool
+ACU_TreeVariableSubproblem::handleBoundStripper(RewritingContext& solution)
 {
+  Assert(solution.value(collectorVarIndex) == nullptr, "collector bound");
+  DagNode* sVal = solution.value(stripperVarIndex);
+  Assert(sVal != nullptr, "stripper not bound");
+  Assert(sVal->symbol() != subject->symbol(), "stripper bound to term headed by top symbol " << sVal);
+  Assert(subject->symbol()->getIdentity() == nullptr || !(subject->symbol()->getIdentity()->equal(sVal)),
+	 "stripper bound to identity " << sVal);
   //
-  //	Take a copy of the remaining arguments tree.
+  //	Stripper variable is bound to an alien. We need to see if we can remove it from remaining
+  //	subject arguments. At most one solution is possible.
   //
-  ACU_Tree t(remaining);
-  //
-  //	Constructively deleted one copy of argument at current path.
-  //	There should still be at least one argument left.
-  //
-  t.deleteMult2(currentPath, 1);
-  Assert(t.getSize() != 0, "no arguments left");
+  currentPath.clear();  // might have had previous solve() calls with other solutions
+  return remaining.find(sVal, currentPath) && bindCollector(solution);
+}
+
+bool
+ACU_TreeVariableSubproblem::bindCollector(RewritingContext& solution)
+{
+  ACU_Tree remainingCopy(remaining);
+  remainingCopy.deleteMult2(currentPath, 1);  // preserves currentPath
+  Assert(remainingCopy.getSize() != 0, "no arguments left");
 
-  DagNode* d;
-  if (t.getSize() == 1 && t.getMaxMult() == 1)
+  DagNode* cVal;
+  if (remainingCopy.getSize() == 1 && remainingCopy.getMaxMult() == 1)
     {
       //
-      //	Only one argument left for collector, so no ACU function symbol on top.
+      //	Just one subject argument left to bind the collector variable to.
+      //	It will already have its correct sort.
       //
-      d = t.getSoleDagNode();
-      if (!leq(d->getSortIndex(), collectorSort))
-	return nullptr;
+      cVal = remainingCopy.getSoleDagNode();
+      if (!leq(cVal->getSortIndex(), collectorSort))
+	return false;
     }
   else
     {
       //
-      //	General case. Make an ACU term with the arguments in t.
+      //	More than one subject argument left; need to make a new ACU_TreeDagNode
+      //	headed by our top symbol.
+      //
+      cVal = new ACU_TreeDagNode(subject->symbol(), remainingCopy);
+      //
+      //	checkSort() could run the garbage collector if sort constraints are executed
+      //	but in this case it will protect cVal in a new context.
       //
-      d = new ACU_TreeDagNode(subject->symbol(), t);
-      if (!(d->checkSort(collectorSort, solution)))
-	return nullptr;
-      if (subject->isReduced() && d->getSortIndex() != Sort::SORT_UNKNOWN)
-	d->setReduced();
+      if (!(cVal->checkSort(collectorSort, solution)))
+	return false;
+      //
+      //	If the parent dagnode was reduced and checkSort() filled in the sort index we
+      //	can mark our binding as reduced.
+      //
+      if (subject->isReduced() && cVal->getSortIndex() != Sort::SORT_UNKNOWN)
+	cVal->setReduced();
     }
-  return d;
+  solution.bind(collectorVarIndex, cVal);
+  return true;
 }
 
 void
 ACU_TreeVariableSubproblem::markReachableNodes()
 {
+  //
+  //	Because remaining may have been made using new dagnodes before it was passed to us
+  //	and the GC can run during the solve phase, we're responsible for protecting it.
+  //
   remaining.mark();
 }
 
diff --git a/src/ACU_Theory/ACU_TreeVariableSubproblem.hh b/src/ACU_Theory/ACU_TreeVariableSubproblem.hh
index 3e6a2016..2611381a 100644
--- a/src/ACU_Theory/ACU_TreeVariableSubproblem.hh
+++ b/src/ACU_Theory/ACU_TreeVariableSubproblem.hh
@@ -31,6 +31,7 @@
 #ifndef _ACU_TreeVariableSubproblem_hh_
 #define _ACU_TreeVariableSubproblem_hh_
 #include "subproblem.hh"
+#include "simpleRootContainer.hh"
 #include "ACU_SlowIter.hh"
 
 class ACU_TreeVariableSubproblem : public Subproblem, private SimpleRootContainer
@@ -38,13 +39,12 @@ class ACU_TreeVariableSubproblem : public Subproblem, private SimpleRootContaine
   NO_COPYING(ACU_TreeVariableSubproblem);
 
 public:
-  ACU_TreeVariableSubproblem(ACU_BaseDagNode* subject,
+  ACU_TreeVariableSubproblem(const ACU_TreeDagNode* subject,
 			     const ACU_Tree& remaining,  // may have red-black nodes not in the subject that we must protect
 			     int stripperVarIndex,
 			     Sort* stripperSort,
 			     int collectorVarIndex,
 			     Sort* collectorSort);
-  ~ACU_TreeVariableSubproblem();
 
   bool solve(bool findFirst, RewritingContext& solution);
 
@@ -54,9 +54,11 @@ public:
 
 private:
   void markReachableNodes();
-  DagNode* collect(RewritingContext& solution);
-
-  ACU_BaseDagNode* const subject;
+  bool handleBoundCollector(RewritingContext& solution);
+  bool handleBoundStripper(RewritingContext& solution);
+  bool bindCollector(RewritingContext& solution);
+  
+  const ACU_BaseDagNode* const subject;
   ACU_Tree remaining;
   const int stripperVarIndex;
   Sort* const stripperSort;
@@ -66,8 +68,12 @@ private:
   //	Solve time variables.
   //
   ACU_SlowIter currentPath;
-  int previousIndex;
-  Vector<LocalBinding*> previous;
+  //
+  //	When ever we look for a first solution, we record whether the stripper and or collector were
+  //	already bound so we can undo any binding we create on future call.
+  //
+  bool stripperAlreadyBound;
+  bool collectorAlreadyBound;
 };
 
 #endif
diff --git a/src/ACU_Theory/ChangeLog b/src/ACU_Theory/ChangeLog
index 015ae7eb..c54cc85f 100755
--- a/src/ACU_Theory/ChangeLog
+++ b/src/ACU_Theory/ChangeLog
@@ -1,3 +1,85 @@
+2023-05-04  Steven Eker  <eker@pup>
+
+	* ACU_TreeVariableSubproblem.cc (ACU_TreeVariableSubproblem::solve): set
+	stripperAlreadyBound, collectorAlreadyBound in findFirst case; otherwise
+	use them to decide whether to clear bindings; this fixes a bug where
+	we were never setting stripperBound to false
+	(ACU_TreeVariableSubproblem::bindCollector): don't set collectorBound
+	(ACU_TreeVariableSubproblem::handleBoundCollector): don't set stripperBound
+	(ACU_TreeVariableSubproblem::handleBoundCollector): added Assert()
+
+	* ACU_TreeVariableSubproblem.hh (class ACU_TreeVariableSubproblem): switched
+	stripperBound -> stripperAlreadyBound, collectorBound ->
+	collectorAlreadyBound
+
+	* ACU_TreeVariableSubproblem.cc (ACU_TreeVariableSubproblem::solve): code
+	cleaning
+	(ACU_TreeVariableSubproblem::handleBoundCollector): fix bug where we were
+	comparing pointer rather that using DagNode::equal()
+	(ACU_TreeVariableSubproblem::handleBoundCollector): code cleaning
+	(ACU_TreeVariableSubproblem::markReachableNodes): added comment
+	(ACU_TreeVariableSubproblem::solve): fix a bug where we never set
+	collectorBound to false
+
+2023-05-02  Steven Eker  <eker@pup>
+
+	* ACU_TreeVariableSubproblem.cc
+	(ACU_TreeVariableSubproblem::handleBoundCollector): don't set oneSolution;
+	set stripperBound if we bind it
+
+	* ACU_TreeVariableSubproblem.hh (class ACU_TreeVariableSubproblem): deleted
+	data member oneSolution
+
+	* ACU_TreeVariableSubproblem.cc (ACU_TreeVariableSubproblem::solve): use
+	stripperBound and collectorBound rather than oneSolution
+
+	* ACU_TreeVariableSubproblem.hh (class ACU_TreeVariableSubproblem): added
+	data members stripperBound and collectorBound
+
+	* ACU_TreeVariableSubproblem.cc	(ACU_TreeVariableSubproblem): Assert()
+	that we have at least two arguments remaining
+	(ACU_TreeVariableSubproblem::handleBoundCollector): rewritten
+
+	* ACU_TreeVariableSubproblem.hh (class ACU_TreeVariableSubproblem):
+	deleted decl for ~ACU_TreeVariableSubproblem()
+
+	* ACU_TreeVariableSubproblem.cc: take const ACU_TreeDagNode*; don't
+	initialized currentPath, previous or previousIndex
+	(ACU_TreeVariableSubproblem::handleBoundStripper): no need to protect
+	new dagnode from GC because checkSort() does this if needed
+	(ACU_TreeVariableSubproblem::bindCollector): ditto
+	(ACU_TreeVariableSubproblem::handleBoundStripper): use bindCollector()
+	(~ACU_TreeVariableSubproblem): deleted
+
+	* ACU_TreeVariableSubproblem.hh (class ACU_TreeVariableSubproblem): added
+	decls for handleBoundCollector(), handleBoundStripper(), bindCollector();
+	deleted decl for collect(); deleted data members previousIndex and
+	previous; added data member oneSolution; updated decl for ctor
+
+	* ACU_TreeVariableSubproblem.cc (ACU_TreeVariableSubproblem::collect):
+	deleted
+	(ACU_TreeVariableSubproblem::handleBoundCollector): added
+	(ACU_TreeVariableSubproblem::handleBoundStripper): added
+	(ACU_TreeVariableSubproblem::bindCollector): added
+	(ACU_TreeVariableSubproblem::solve): reimplemented using
+	handleBoundCollector(), handleBoundStripper() and bindCollector(); don't
+	cache previous solutions; fix bug where we were not protecting newly
+	created ACU_TreeDagNode from the garbage collector during checkSort()
+
+2023-05-01  Steven Eker  <eker@pup>
+
+	* ACU_LhsAutomaton.cc (ACU_LhsAutomaton::complete): fix bug by doing
+	stripper/collector calculations here, after variables have been sorted
+	(ACU_LhsAutomaton::addTopVariable): don't do stripper/collector
+	calculations here
+	(ACU_LhsAutomaton::addTopVariable): store willBeBound
+
+	* ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added data member
+	willBeBound to struct TopVariable; rearrange data members of
+	struct TopVariable
+
+===================================Maude148===========================================
+
 2023-04-28  Steven Eker  <eker@pup>
 
 	* ACU_TreeMatcher.cc (ACU_LhsAutomaton::loneSubjectNGA_Case): need to
diff --git a/src/Core/ChangeLog b/src/Core/ChangeLog
index b5f9ac01..de51809c 100644
--- a/src/Core/ChangeLog
+++ b/src/Core/ChangeLog
@@ -1,3 +1,29 @@
+2023-05-04  Steven Eker  <eker@pup>
+
+	* memoryCell.cc: added constants SMALL_MODEL_SLOP, BIG_MODEL_SLOP,
+	LOWER_BOUND, UPPER_BOUND; deleted constant NODE_MULTIPLIER
+	(MemoryCell::collectGarbage): try dynamic scaling of slopFactor
+
+2023-05-03  Steven Eker  <eker@pup>
+
+	* memoryCell.cc: moved NODE_MULTIPLIER here
+
+	* memoryCell.hh (MemoryCell::setEarlyQuit): added
+
+	* memoryCell.cc (MemoryCell::collectGarbage): support earlyQuit
+
+	* memoryCell.hh (class MemoryCell): added static data member earlyQuit
+
+	* memoryCell.cc (MemoryCell::collectGarbage): keep track of number of
+	garbage collects
+	(MemoryCell::collectGarbage): translate numbers to MBs
+
+	* memoryCell.hh (class MemoryCell): added NODE_MULTIPLIER
+
+	* memoryCell.cc (MemoryCell::collectGarbage): use NODE_MULTIPLIER
+
+===================================Maude148===========================================
+
 2023-04-13  Steven Eker  <eker@pup>
 
 	* preEquation.cc (PreEquation::checkCondition): use empty()
@@ -2042,7 +2068,7 @@
 
 	* unificationSubproblemDisjunction.hh (class
 	UnificationSubproblemDisjunction): updated decl for
-	UnificationSubproblemDisjunction() 
+	UnificationSubproblemDisjunction()
 
 	* unificationSubproblemDisjunction.cc
 	(UnificationSubproblemDisjunction): take nrBinding arg
@@ -2820,7 +2846,7 @@
 
 	* equationTable.cc (applyReplace): DagNode::okToCollectGarbage()
 	-> MemoryCell::okToCollectGarbage()
-	
+
 ===================================Maude78===========================================
 
 2003-01-08  Steven Eker  <eker@goo.csl.sri.com>
@@ -2850,13 +2876,13 @@
 	* preEquation.cc (cleanStack): created
 	(checkCondition): call cleanStack() before returning to to an
 	abort
-	
+
 2002-11-20  Steven Eker  <eker@goo.csl.sri.com>
 
 	* checkedArgVecConstIterator.hh (operator->): made const
 	(operator*): made const
 	(class const_iterator): updated decls for operator*() and
-	operator->() 
+	operator->()
 
 	* checkedArgVecIterator.hh (class iterator): make const_iterator a
 	friend
@@ -2884,7 +2910,7 @@
 
 	* argVec.hh: major rewrite to make it look more STL like and
 	support iterators
-	
+
 ===================================Maude77==================================================
 
 2002-11-15  Steven Eker  <eker@goo.csl.sri.com>
@@ -7016,7 +7042,6 @@ Wed Dec 13 11:54:57 1995  Steven Eker  <eker@ponder.csl.sri.com>
 	(dumpSort): added
 
 	* connectedComponent.hh: added dumpSort()
-	
 
 Fri Dec  8 10:04:56 1995  Steven Eker  <eker@ponder.csl.sri.com>
 
diff --git a/src/Core/memoryCell.cc b/src/Core/memoryCell.cc
index 145cb5f6..45e79b9c 100644
--- a/src/Core/memoryCell.cc
+++ b/src/Core/memoryCell.cc
@@ -2,7 +2,7 @@
 
     This file is part of the Maude 3 interpreter.
 
-    Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
+    Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA.
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -23,6 +23,7 @@
 //
 //      Implementation for base class MemoryCell
 //
+#include "cmath"
 
 //	utility stuff
 #include "macros.hh"
@@ -38,6 +39,14 @@
 
 #include "memoryCell.hh"
 
+//static constexpr int  NODE_MULTIPLIER = 8;	// after GC increase arenas so we have (NODE_MULTIPLIER - 1) * used-nodes
+
+static constexpr double SMALL_MODEL_SLOP = 8.0;
+static constexpr double BIG_MODEL_SLOP = 2.0;
+static constexpr int64_t LOWER_BOUND = 4 * 1024 * 1024;  // use small model if <= 4 million nodes
+static constexpr int64_t UPPER_BOUND = 32 * 1024 * 1024;  // use big model if >= 32 million nodes
+
+
 struct MemoryCell::Arena
 {
   union
@@ -56,6 +65,8 @@ MemoryCell::Arena::firstNode()
 }
 
 bool MemoryCell::showGC = false;
+int64_t MemoryCell::earlyQuit = 0;
+
 //
 //	Arena management variables.
 //
@@ -296,6 +307,8 @@ MemoryCell::tidyArenas()
 void
 MemoryCell::collectGarbage()
 {
+  static int64_t gcCount = 0;
+
   if (firstArena == 0)
     return;
   tidyArenas();
@@ -327,23 +340,36 @@ MemoryCell::collectGarbage()
   //	Calculate if we should allocate more arenas to avoid an early gc.
   //
   int nrNodes = nrArenas * ARENA_SIZE;
+  ++gcCount;
   if (showGC)
     {
-      cout << "Arenas: " << nrArenas <<
-	"\tNodes: " << nrNodes <<
-	//	"\tIn use: " << nrNodesInUse <<
-	//	"\tCollected: " << reclaimed << 
+      cout << "Collection: " << gcCount << "\n";
+      
+      cout << "Arenas: " << nrArenas << "\tNodes: " << nrNodes <<
+	" (" << double(nrNodes * sizeof(MemoryCell))/(1024.0 * 1024.0) << " MB)" <<
 	"\tNow: " << nrNodesInUse <<
-	"\nBuckets: " << nrBuckets <<
-	"\tBytes: " << bucketStorage <<
+	" (" << double(nrNodesInUse * sizeof(MemoryCell))/(1024.0 * 1024.0) << " MB)" << "\n";
+      
+      cout << "Buckets: " << nrBuckets << "\tBytes: " << bucketStorage <<
+	" (" << double(bucketStorage) / (1024.0 * 1024.0) << " MB)" <<
 	"\tIn use: " << oldStorageInUse <<
+	" (" << double(oldStorageInUse) / (1024.0 * 1024.0) << " MB)" <<
 	"\tCollected: " << oldStorageInUse - storageInUse <<
-	"\tNow: " << storageInUse << '\n';
+	" (" << double(oldStorageInUse - storageInUse) / (1024.0 * 1024.0) << " MB)" <<
+	"\tNow: " << storageInUse <<
+	" (" << double(storageInUse) / (1024.0 * 1024.0) << " MB)" << "\n";
     }
+  if (gcCount == earlyQuit)
+    exit(0);
+  double slopFactor = BIG_MODEL_SLOP;  // if we are using lots of nodes
+  if (nrNodesInUse <= LOWER_BOUND)
+    slopFactor = SMALL_MODEL_SLOP;  // if we are using few nodes
+  else if (nrNodesInUse < UPPER_BOUND)
+    slopFactor += ((UPPER_BOUND - nrNodesInUse) * (SMALL_MODEL_SLOP - BIG_MODEL_SLOP)) / (UPPER_BOUND - LOWER_BOUND);
   //
-  //	Allocate new arenas so that we have at least 50% of nodes unused.
+  //	Allocate new arenas so that we have at least slopFactor times the actually used nodes.
   //
-  int neededArenas = ceilingDivision(2 * nrNodesInUse, ARENA_SIZE);
+  int neededArenas = ceil((slopFactor * nrNodesInUse) / ARENA_SIZE);
   while (nrArenas < neededArenas)
     (void) allocateNewArena();
   //
diff --git a/src/Core/memoryCell.hh b/src/Core/memoryCell.hh
index 0fdf3bc7..12bdceac 100644
--- a/src/Core/memoryCell.hh
+++ b/src/Core/memoryCell.hh
@@ -2,7 +2,7 @@
 
     This file is part of the Maude 3 interpreter.
 
-    Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
+    Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA.
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -60,7 +60,7 @@ public:
   static void collectGarbage();
 
   static void setShowGC(bool polarity);
-
+  static void setEarlyQuit(int64_t count);
   //
   //	We provide functions for getting access to the MemoryInfo object
   //	corresponding the a memory block we allocated.
@@ -84,6 +84,7 @@ private:
   struct Bucket;		// bucket of variable length allocations
 
   static bool showGC;		// do we report GC stats to user
+  static int64_t earlyQuit;	// do we quit early for profiling purposes
   //
   //	Arena management variables.
   //
@@ -169,6 +170,12 @@ MemoryCell::setShowGC(bool polarity)
   showGC = polarity;
 }
 
+inline void
+MemoryCell::setEarlyQuit(int64_t count)
+{
+  earlyQuit = count;
+}
+
 inline void*
 MemoryCell::allocateMemoryCell()
 {
diff --git a/src/Main/ChangeLog b/src/Main/ChangeLog
index bcfb6b85..152ca8ea 100755
--- a/src/Main/ChangeLog
+++ b/src/Main/ChangeLog
@@ -1,3 +1,14 @@
+2023-05-05  Steven Eker  <eker@pup>
+
+	* main.cc (printHelp): document -early-quit=N and make use of adjacent
+	string concatenation
+
+2023-05-03  Steven Eker  <eker@pup>
+
+	* main.cc (main): added -early-quit
+
+===================================Maude148===========================================
+
 2023-03-03  Steven Eker  <eker@pup>
 
 	* prelude.maude: update version number
diff --git a/src/Main/main.cc b/src/Main/main.cc
index cfb0d45f..1348b9a3 100755
--- a/src/Main/main.cc
+++ b/src/Main/main.cc
@@ -50,6 +50,7 @@
  
 //      core class definitions
 #include "lineNumber.hh"
+#include "memoryCell.hh"
 
 //      built class definitions
 #include "randomOpSymbol.hh"
@@ -171,6 +172,8 @@ main(int argc, char* argv[])
 	      DirectoryManagerSymbol::setAllowDir(true);
 	      ProcessManagerSymbol::setAllowProcesses(true);
 	    }
+	  else if (const char* s = isFlag(arg, "-early-quit="))
+	    MemoryCell::setEarlyQuit(strtoul(s, 0, 0));
 	  else
 	    {
 	      IssueWarning(LineNumber(FileTable::COMMAND_LINE) <<
@@ -276,35 +279,37 @@ void
 printHelp(const char* name)
 {
   cout <<
-    "Maude interpreter\n" <<
-    "Usage: " << name << " [options] [files]\n" <<
-    "Options:\n" <<
-    "  --help\t\tDisplay this information\n" <<
-    "  --version\t\tDisplay version number\n" <<
-    "  -no-prelude\t\tDo not read in the standard prelude\n" <<
-    "  -no-banner\t\tDo not output banner on startup\n" <<
-    "  -no-advise\t\tNo advisories on startup\n" <<
-    "  -always-advise\tAlways show advisories regardless\n" <<
-    "  -no-mixfix\t\tDo not use mixfix notation for output\n" <<
-    "  -no-wrap\t\tDo not use automatic line wrapping for output\n" <<
-    "  -ansi-color\t\tUse ANSI control sequences\n" <<
-    "  -no-ansi-color\tDo not use ANSI control sequences\n" <<
-    "  -tecla\t\tUse tecla command line editing\n" <<
-    "  -no-tecla\t\tDo not use tecla command line editing\n" <<
-    "  -batch\t\tRun in batch mode\n" <<
-    "  -interactive\t\tRun in interactive mode\n" <<
-    "  -print-to-stderr\tPrint attribute should use stderr rather than stdout\n" <<
-    "  -random-seed=<int>\tSet seed for random number generator\n" <<
-    "  -xml-log=<filename>\tSet file in which to produce an xml log\n" <<
-    "  -show-pid\t\tPrint process id to stderr before printing banner\n" <<
-    "  -erewrite-loop-mode\tUse external object rewriting for loop mode\n" <<
-    "  -allow-processes\tAllow running arbitrary executables\n" <<
-    "  -allow-files\t\tAllow operations on files\n" <<
-    "  -allow-dir\t\tAllow operations on directories\n" <<
-    "  -trust\t\tAllow all potentially risky capabilities\n" <<
+    "Maude interpreter\n"
+    "Usage: " << name << " [options] [files]\n"
+    "Options:\n"
+    "  --help\t\tDisplay this information\n"
+    "  --version\t\tDisplay version number\n"
+    "  -no-prelude\t\tDo not read in the standard prelude\n"
+    "  -no-banner\t\tDo not output banner on startup\n"
+    "  -no-advise\t\tNo advisories on startup\n"
+    "  -always-advise\tAlways show advisories regardless\n"
+    "  -no-mixfix\t\tDo not use mixfix notation for output\n"
+    "  -no-wrap\t\tDo not use automatic line wrapping for output\n"
+    "  -ansi-color\t\tUse ANSI control sequences\n"
+    "  -no-ansi-color\tDo not use ANSI control sequences\n"
+    "  -tecla\t\tUse tecla command line editing\n"
+    "  -no-tecla\t\tDo not use tecla command line editing\n"
+    "  -batch\t\tRun in batch mode\n"
+    "  -interactive\t\tRun in interactive mode\n"
+    "  -print-to-stderr\tPrint attribute should use stderr rather than stdout\n"
+    "  -random-seed=<int>\tSet seed for random number generator\n"
+    "  -xml-log=<filename>\tSet file in which to produce an xml log\n"
+    "  -show-pid\t\tPrint process id to stderr before printing banner\n"
+    "  -erewrite-loop-mode\tUse external object rewriting for loop mode\n"
+    "  -allow-processes\tAllow running arbitrary executables\n"
+    "  -allow-files\t\tAllow operations on files\n"
+    "  -allow-dir\t\tAllow operations on directories\n"
+    "  -trust\t\tAllow all potentially risky capabilities\n"
     "  -assoc-unif-depth=<float>\tSet depth bound multiplier for associative unification\n"
+    "Intended for developer use:\n"
     "  -debug\t\tPrint copious messages about internal state (debug build only)\n"
-    "\n" <<
+    "  -early-quit=<int>\tQuit abruptly after a given number of garbage collections\n"
+    "\n"
     "Send bug reports to: " << PACKAGE_BUGREPORT << endl;
   exit(0);
 }
diff --git a/src/Meta/ChangeLog b/src/Meta/ChangeLog
index 0c7efd8b..902e8ca3 100644
--- a/src/Meta/ChangeLog
+++ b/src/Meta/ChangeLog
@@ -1,3 +1,29 @@
+2023-05-05  Steven Eker  <eker@pup>
+
+	* remoteInterpreter2.cc: use static constexpr rather than define for
+	EOT
+
+	* miRewrite.cc (InterpreterManagerSymbol::srewriteTerm):  fix bug where
+	rewrite count was only being transfered in failure case
+
+2023-05-04  Steven Eker  <eker@pup>
+
+	* metaSrewrite.cc (MetaLevelOpSymbol::metaSrewrite): fix bug where we
+	we not transferring rewrite count to context
+
+2023-05-02  Steven Eker  <eker@pup>
+
+	* metaModuleCache.hh (class MetaModuleCache): deleted decl for equal()
+
+2023-05-01  Steven Eker  <eker@pup>
+
+	* metaModuleCache.cc (MetaModuleCache::find): revert
+	(MetaModuleCache::equal): deleted
+
+	* metaModuleCache.hh (class MetaModuleCache): added decl for equal()
+
+	* metaModuleCache.cc (MetaModuleCache::equal): added
+
 2023-04-26  Steven Eker  <eker@pup>
 
 	* metaMatch.cc (MetaLevelOpSymbol::metaMatch): reverted; passing solutionNr
diff --git a/src/Meta/metaModuleCache.cc b/src/Meta/metaModuleCache.cc
index c8d2eacc..8f32c171 100644
--- a/src/Meta/metaModuleCache.cc
+++ b/src/Meta/metaModuleCache.cc
@@ -31,6 +31,7 @@
 //      forward declarations
 #include "interface.hh"
 #include "core.hh"
+#include "freeTheory.hh"
 #include "higher.hh"
 #include "strategyLanguage.hh"
 #include "mixfix.hh"
@@ -42,6 +43,10 @@
 //      core class definitions
 #include "dagRoot.hh"
 
+//      free theory class definitions
+#include "freeSymbol.hh"
+#include "freeDagNode.hh"
+
 //	front end class definitions
 #include "metaModule.hh"
 #include "metaModuleCache.hh"
@@ -81,6 +86,7 @@ MetaModuleCache::Pair::clear()
   t->deepSelfDestruct();
 }
 
+
 MetaModule*
 MetaModuleCache::find(DagNode* dag)
 {
diff --git a/src/Meta/metaSrewrite.cc b/src/Meta/metaSrewrite.cc
index 73e82f69..4a6c2db8 100644
--- a/src/Meta/metaSrewrite.cc
+++ b/src/Meta/metaSrewrite.cc
@@ -45,6 +45,7 @@ MetaLevelOpSymbol::metaSrewrite(FreeDagNode* subject,
 	  while (lastSolutionNr < solutionNr)
 	    {
 	      result = state->findNextSolution();
+	      context.transferCountFrom(*(state->getContext()));
 	      if (result == 0)
 		{
 		  delete state;
diff --git a/src/Meta/miRewrite.cc b/src/Meta/miRewrite.cc
index 97470742..967d64dc 100644
--- a/src/Meta/miRewrite.cc
+++ b/src/Meta/miRewrite.cc
@@ -331,6 +331,7 @@ InterpreterManagerSymbol::srewriteTerm(FreeDagNode* message,
 	      PointerMap dagNodeMap;
 	      args[3] = metaLevel->upDagNode(result, mm, qidMap, dagNodeMap);
 	      args[4] = metaLevel->upType(result->getSort(), qidMap);
+	      context.transferCountFrom(*(state->getContext()));
 	      (void) mm->unprotect();
 	      return srewroteTermMsg->makeDagNode(args);
 	    }
diff --git a/src/Meta/remoteInterpreter.cc b/src/Meta/remoteInterpreter.cc
index b1ba7f0e..1f8d1e1e 100644
--- a/src/Meta/remoteInterpreter.cc
+++ b/src/Meta/remoteInterpreter.cc
@@ -110,7 +110,7 @@ InterpreterManagerSymbol::createRemoteInterpreter(FreeDagNode* originalMessage,
       return true;
     }
   //
-  //	For a new Maude interpreter.
+  //	Fork a new Maude interpreter.
   //
   pid_t pid = fork();
   if (pid == -1)
@@ -134,7 +134,7 @@ InterpreterManagerSymbol::createRemoteInterpreter(FreeDagNode* originalMessage,
       //
       UserLevelRewritingContext::ignoreCtrlC();  // don't respond to ctrl-C
       extern IO_Manager ioManager;  // HACK
-      ioManager.unsetAutoWrap();  // don't to wrapping on our output
+      ioManager.unsetAutoWrap();  // don't do wrapping on our output
       //globalAdvisoryFlag = false;  // limit crap that we dump on screen
       close(ioSockets[0]);
       close(errSockets[0]);  // close parent end
diff --git a/src/Meta/remoteInterpreter2.cc b/src/Meta/remoteInterpreter2.cc
index e35d325d..b9464081 100644
--- a/src/Meta/remoteInterpreter2.cc
+++ b/src/Meta/remoteInterpreter2.cc
@@ -2,7 +2,7 @@
 
     This file is part of the Maude 3 interpreter.
 
-    Copyright 2020 SRI International, Menlo Park, CA 94025, USA.
+    Copyright 2020-2023 SRI International, Menlo Park, CA 94025, USA.
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -23,7 +23,7 @@
 //
 //      Remote metaInterpreters: child side
 //
-#define EOT '\004'
+static constexpr char EOT = '\004';
 
 Rope
 InterpreterManagerSymbol::receiveMessage(int socketId)
diff --git a/src/Utility/ChangeLog b/src/Utility/ChangeLog
index c07e4484..0f65696e 100644
--- a/src/Utility/ChangeLog
+++ b/src/Utility/ChangeLog
@@ -1,3 +1,9 @@
+2023-05-01  Steven Eker  <eker@pup>
+
+	* macros.hh: added Profile() macro
+
+===================================Maude148===================================
+
 2023-04-13  Steven Eker  <eker@pup>
 
 	* intSet.cc (IntSet::findEntry): use empty()
diff --git a/src/Utility/macros.hh b/src/Utility/macros.hh
index 703e1ff1..ea9f289b 100644
--- a/src/Utility/macros.hh
+++ b/src/Utility/macros.hh
@@ -190,6 +190,20 @@ safeCastNonNull(P p)
   return static_cast<T>(p);
 }
 
+template <typename T, typename P>
+inline T
+downCast(P p)
+{
+#ifndef NO_ASSERT
+  if (dynamic_cast<T>(p) == 0)
+    {
+      cerr << "unexpected null or cast error: "<< __FILE__ << ':' << __LINE__ << '\n';
+      abort();
+    }
+#endif
+  return static_cast<T>(p);
+}
+
 enum SpecialConstants
 {
   NR_PTR_LOSE_BITS = 3,		// number of rhs bits to chop when hashing a pointer
@@ -392,6 +406,19 @@ Verbose(output) \
 if (globalVerboseFlag) \
   (cerr << Tty(Tty::CYAN) << output << Tty(Tty::RESET) << '\n')
 
+#ifdef PROFILING
+
+#define \
+Profile(color, message) \
+  (cerr << Tty(Tty::color) << message << Tty(Tty::RESET))
+
+#else
+
+#define \
+Profile(color, message)
+
+#endif
+
 extern bool globalAdvisoryFlag;
 extern bool globalVerboseFlag;
 extern bool globalDebugFlag;
diff --git a/tests/Corner/ACU_TreeVariableSubproblem b/tests/Corner/ACU_TreeVariableSubproblem
new file mode 100755
index 00000000..0c542cce
--- /dev/null
+++ b/tests/Corner/ACU_TreeVariableSubproblem
@@ -0,0 +1,10 @@
+#!/bin/sh
+
+MAUDE_LIB=$srcdir/../../src/Main
+export MAUDE_LIB
+
+../../src/Main/maude \
+  < $srcdir/ACU_TreeVariableSubproblem.maude -no-banner \
+  > ACU_TreeVariableSubproblem.out 2>&1
+
+diff $srcdir/ACU_TreeVariableSubproblem.expected ACU_TreeVariableSubproblem.out > /dev/null 2>&1
diff --git a/tests/Corner/ACU_TreeVariableSubproblem.expected b/tests/Corner/ACU_TreeVariableSubproblem.expected
new file mode 100644
index 00000000..430f1dd9
--- /dev/null
+++ b/tests/Corner/ACU_TreeVariableSubproblem.expected
@@ -0,0 +1,81 @@
+==========================================
+reduce in FOO : h(g(11), g(11)) .
+rewrites: 25
+result NzNat: 11
+==========================================
+reduce in FOO : h(f(g(9), g(11)), f(g(9), g(11))) .
+rewrites: 35
+result NzNat: 11
+Advisory: redefining module FOO.
+==========================================
+reduce in FOO : h(g(11), g(11)) .
+rewrites: 14
+result Zero: 0
+==========================================
+reduce in FOO : h(f(g(9), g(11)), f(g(9), g(11))) .
+rewrites: 24
+result Zero: 0
+Advisory: redefining module FOO.
+==========================================
+reduce in FOO : h(g(11), g(11)) .
+rewrites: 13
+result NzNat: 5
+==========================================
+reduce in FOO : h(f(g(9), g(11)), f(g(9), g(11))) .
+rewrites: 23
+result NzNat: 5
+Advisory: redefining module FOO.
+==========================================
+reduce in FOO : h(g(11), g(11)) .
+rewrites: 25
+result Set: f(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10)
+==========================================
+reduce in FOO : h(f(g(9), g(11)), f(g(9), g(11))) .
+rewrites: 35
+result Set: f(0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6, 7, 7, 8, 8, 9, 9, 10)
+Advisory: redefining module FOO.
+==========================================
+reduce in FOO : h(g(11), g(11)) .
+rewrites: 14
+result Set: f(1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11)
+==========================================
+reduce in FOO : h(f(g(9), g(11)), f(g(9), g(11))) .
+rewrites: 24
+result Set: f(0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6, 7, 7, 8, 8, 9, 9, 10, 11)
+Advisory: redefining module FOO.
+==========================================
+reduce in FOO : h(g(11), g(11)) .
+rewrites: 13
+result Set: f(0, 1, 2, 3, 4, 6, 7, 8, 9, 10, 11)
+==========================================
+reduce in FOO : h(f(g(9), g(11)), f(g(9), g(11))) .
+rewrites: 23
+result Set: f(0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 6, 6, 7, 7, 8, 8, 9, 9, 10, 11)
+Advisory: redefining module FOO.
+==========================================
+reduce in FOO : h(g(11), g(11)) .
+rewrites: 25
+result Set: f(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10)
+==========================================
+reduce in FOO : h(f(g(9), g(11)), f(g(9), g(11))) .
+rewrites: 35
+result Set: f(0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6, 7, 7, 8, 8, 9, 9, 10)
+Advisory: redefining module FOO.
+==========================================
+reduce in FOO : h(g(11), g(11)) .
+rewrites: 14
+result Set: f(1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11)
+==========================================
+reduce in FOO : h(f(g(9), g(11)), f(g(9), g(11))) .
+rewrites: 24
+result Set: f(0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6, 7, 7, 8, 8, 9, 9, 10, 11)
+Advisory: redefining module FOO.
+==========================================
+reduce in FOO : h(g(11), g(11)) .
+rewrites: 13
+result Set: f(0, 1, 2, 3, 4, 6, 7, 8, 9, 10, 11)
+==========================================
+reduce in FOO : h(f(g(9), g(11)), f(g(9), g(11))) .
+rewrites: 23
+result Set: f(0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 6, 6, 7, 7, 8, 8, 9, 9, 10, 11)
+Bye.
diff --git a/tests/Corner/ACU_TreeVariableSubproblem.maude b/tests/Corner/ACU_TreeVariableSubproblem.maude
new file mode 100644
index 00000000..846e10cc
--- /dev/null
+++ b/tests/Corner/ACU_TreeVariableSubproblem.maude
@@ -0,0 +1,187 @@
+set show timing off .
+
+***
+***	Check corner cases for class ACU_TreeVariableSubproblem.
+***
+***	This kind of matching subproblem is generated when we have unbound stripper and collector
+***	variables, the subject is in red-black tree form, and we need to generate all solutions.
+***	Corner cases arise when the stripper and/or collector variable is bound by an earlier
+*** 	ACU_TreeVariableSubproblem and we need to deal with the bound variables correctly.
+***
+
+*** bound collector case
+
+fmod FOO is
+  pr NAT .
+  sort  Set .
+  subsort Nat < Set .
+var N M : Nat .
+  op f : Set Set -> Set [assoc comm] .
+  op g : Nat -> Set .
+  eq g(0) = 0 .
+  eq g(s N) = f(g(N), s N) .  *** make a red-black tree of arguments
+
+var S : Set .
+  op h : Set Set -> Set .
+  ceq h(f(N, S), f(M, S)) = M if N > 10 .  *** N, M are strippers, S is a collector
+endfm
+
+red h(g(11), g(11)) .
+red h(f(g(11), g(9)), f(g(11), g(9))) .  *** multiplicities > 1
+
+
+fmod FOO is
+  pr NAT .
+  sort  Set .
+  subsort Nat < Set .
+var N M : Nat .
+  op f : Set Set -> Set [assoc comm] .
+  op g : Nat -> Set .
+  eq g(0) = 0 .
+  eq g(s N) = f(g(N), s N) .  *** make a red-black tree of arguments
+
+var S : Set .
+  op h : Set Set -> Set .
+  ceq h(f(N, S), f(M, S)) = M if N < 2 .  *** N, M are strippers, S is a collector
+endfm
+
+red h(g(11), g(11)) .
+red h(f(g(11), g(9)), f(g(11), g(9))) .  *** multiplicities > 1
+
+
+fmod FOO is
+  pr NAT .
+  sort  Set .
+  subsort Nat < Set .
+var N M : Nat .
+  op f : Set Set -> Set [assoc comm] .
+  op g : Nat -> Set .
+  eq g(0) = 0 .
+  eq g(s N) = f(g(N), s N) .  *** make a red-black tree of arguments
+
+var S : Set .
+  op h : Set Set -> Set .
+  ceq h(f(N, S), f(M, S)) = M if N = 5 .  *** N, M are strippers, S is a collector
+endfm
+
+red h(g(11), g(11)) .
+red h(f(g(11), g(9)), f(g(11), g(9))) .  *** multiplicities > 1
+
+
+
+*** bound stripper case
+
+fmod FOO is
+  pr NAT .
+  sort  Set .
+  subsort Nat < Set .
+var N : Nat .
+  op f : Set Set -> Set [assoc comm] .
+  op g : Nat -> Set .
+  eq g(0) = 0 .
+  eq g(s N) = f(g(N), s N) .  *** make a red-black tree of arguments
+
+var S T : Set .
+  op h : Set Set -> Set .
+  ceq h(f(N, S), f(N, T)) = T if N > 10 .  *** N is a strippers, S, T are collectors
+endfm
+
+red h(g(11), g(11)) .
+red h(f(g(11), g(9)), f(g(11), g(9))) .  *** multiplicities > 1
+
+
+fmod FOO is
+  pr NAT .
+  sort  Set .
+  subsort Nat < Set .
+var N : Nat .
+  op f : Set Set -> Set [assoc comm] .
+  op g : Nat -> Set .
+  eq g(0) = 0 .
+  eq g(s N) = f(g(N), s N) .  *** make a red-black tree of arguments
+
+var S T : Set .
+  op h : Set Set -> Set .
+  ceq h(f(N, S), f(N, T)) = T if N < 2 .  *** N is a strippers, S, T are collectors
+endfm
+
+red h(g(11), g(11)) .
+red h(f(g(11), g(9)), f(g(11), g(9))) .  *** multiplicities > 1
+
+
+fmod FOO is
+  pr NAT .
+  sort  Set .
+  subsort Nat < Set .
+var N : Nat .
+  op f : Set Set -> Set [assoc comm] .
+  op g : Nat -> Set .
+  eq g(0) = 0 .
+  eq g(s N) = f(g(N), s N) .  *** make a red-black tree of arguments
+
+var S T : Set .
+  op h : Set Set -> Set .
+  ceq h(f(N, S), f(N, T)) = T if N = 5 .  *** N is a strippers, S, T are collectors
+endfm
+
+red h(g(11), g(11)) .
+red h(f(g(11), g(9)), f(g(11), g(9))) .  *** multiplicities > 1
+
+
+*** both bound case
+
+fmod FOO is
+  pr NAT .
+  sort  Set .
+  subsort Nat < Set .
+var N : Nat .
+  op f : Set Set -> Set [assoc comm] .
+  op g : Nat -> Set .
+  eq g(0) = 0 .
+  eq g(s N) = f(g(N), s N) .  *** make a red-black tree of arguments
+
+var S T : Set .
+  op h : Set Set -> Set .
+  ceq h(f(N, S), f(N, S)) = S if N > 10 .  *** N is a strippers, S is a collector
+endfm
+
+red h(g(11), g(11)) .
+red h(f(g(11), g(9)), f(g(11), g(9))) .  *** multiplicities > 1
+
+
+fmod FOO is
+  pr NAT .
+  sort  Set .
+  subsort Nat < Set .
+var N : Nat .
+  op f : Set Set -> Set [assoc comm] .
+  op g : Nat -> Set .
+  eq g(0) = 0 .
+  eq g(s N) = f(g(N), s N) .  *** make a red-black tree of arguments
+
+var S : Set .
+  op h : Set Set -> Set .
+  ceq h(f(N, S), f(N, S)) = S if N < 2 .  *** N is a strippers, S is a collector
+endfm
+
+red h(g(11), g(11)) .
+red h(f(g(11), g(9)), f(g(11), g(9))) .  *** multiplicities > 1
+
+
+fmod FOO is
+  pr NAT .
+  sort  Set .
+  subsort Nat < Set .
+var N : Nat .
+  op f : Set Set -> Set [assoc comm] .
+  op g : Nat -> Set .
+  eq g(0) = 0 .
+  eq g(s N) = f(g(N), s N) .  *** make a red-black tree of arguments
+
+var S : Set .
+  op h : Set Set -> Set .
+  ceq h(f(N, S), f(N, S)) = S if N = 5 .  *** N is a strippers, S is a collector
+endfm
+
+red h(g(11), g(11)) .
+red h(f(g(11), g(9)), f(g(11), g(9))) .  *** multiplicities > 1
diff --git a/tests/Corner/Makefile.am b/tests/Corner/Makefile.am
index ac7fa823..1f56c1d8 100644
--- a/tests/Corner/Makefile.am
+++ b/tests/Corner/Makefile.am
@@ -5,7 +5,8 @@ TESTS = \
 	badStatement \
 	fakeParameterSort \
 	fakeParameterConstant \
-	attributeOverparsing
+	attributeOverparsing \
+	ACU_TreeVariableSubproblem
 
 MAUDE_FILES = \
 	badOmod.maude \
@@ -14,7 +15,8 @@ MAUDE_FILES = \
 	badStatement.maude \
 	fakeParameterSort.maude \
 	fakeParameterConstant.maude \
-	attributeOverparsing.maude
+	attributeOverparsing.maude \
+	ACU_TreeVariableSubproblem.maude
 
 RESULT_FILES = \
 	badOmod.expected \
@@ -23,6 +25,7 @@ RESULT_FILES = \
 	badStatement.expected \
 	fakeParameterSort.expected \
 	fakeParameterConstant.expected \
-	attributeOverparsing.expected
+	attributeOverparsing.expected \
+	ACU_TreeVariableSubproblem.expected
 
 EXTRA_DIST = $(TESTS) $(MAUDE_FILES) $(RESULT_FILES)
diff --git a/tests/Corner/Makefile.in b/tests/Corner/Makefile.in
index 288c1247..b8d2a6e8 100644
--- a/tests/Corner/Makefile.in
+++ b/tests/Corner/Makefile.in
@@ -442,7 +442,8 @@ TESTS = \
 	badStatement \
 	fakeParameterSort \
 	fakeParameterConstant \
-	attributeOverparsing
+	attributeOverparsing \
+	ACU_TreeVariableSubproblem
 
 MAUDE_FILES = \
 	badOmod.maude \
@@ -451,7 +452,8 @@ MAUDE_FILES = \
 	badStatement.maude \
 	fakeParameterSort.maude \
 	fakeParameterConstant.maude \
-	attributeOverparsing.maude
+	attributeOverparsing.maude \
+	ACU_TreeVariableSubproblem.maude
 
 RESULT_FILES = \
 	badOmod.expected \
@@ -460,7 +462,8 @@ RESULT_FILES = \
 	badStatement.expected \
 	fakeParameterSort.expected \
 	fakeParameterConstant.expected \
-	attributeOverparsing.expected
+	attributeOverparsing.expected \
+	ACU_TreeVariableSubproblem.expected
 
 EXTRA_DIST = $(TESTS) $(MAUDE_FILES) $(RESULT_FILES)
 all: all-am
@@ -693,6 +696,13 @@ attributeOverparsing.log: attributeOverparsing
 	--log-file $$b.log --trs-file $$b.trs \
 	$(am__common_driver_flags) $(AM_LOG_DRIVER_FLAGS) $(LOG_DRIVER_FLAGS) -- $(LOG_COMPILE) \
 	"$$tst" $(AM_TESTS_FD_REDIRECT)
+ACU_TreeVariableSubproblem.log: ACU_TreeVariableSubproblem
+	@p='ACU_TreeVariableSubproblem'; \
+	b='ACU_TreeVariableSubproblem'; \
+	$(am__check_pre) $(LOG_DRIVER) --test-name "$$f" \
+	--log-file $$b.log --trs-file $$b.trs \
+	$(am__common_driver_flags) $(AM_LOG_DRIVER_FLAGS) $(LOG_DRIVER_FLAGS) -- $(LOG_COMPILE) \
+	"$$tst" $(AM_TESTS_FD_REDIRECT)
 .test.log:
 	@p='$<'; \
 	$(am__set_b); \
diff --git a/tests/Meta/metaIntStrategy.expected b/tests/Meta/metaIntStrategy.expected
index b639d424..9a45f7b9 100644
--- a/tests/Meta/metaIntStrategy.expected
+++ b/tests/Meta/metaIntStrategy.expected
@@ -8,7 +8,7 @@ result Configuration: <> < me : User | option: breadthFirst, output: ('__[
     'I.RomanSymbol,'I.RomanSymbol,'I.RomanSymbol,'I.RomanSymbol]), solcount: 1,
     input: '__['M.RomanSymbol,'C.RomanSymbol,'M.RomanSymbol,'X.RomanSymbol,
     'C.RomanSymbol,'I.RomanSymbol,'X.RomanSymbol] @ 'additive-normal-form[[
-    empty]] > noSuchResult(me, interpreter(0), 105)
+    empty]] > noSuchResult(me, interpreter(0), 0)
 ==========================================
 erewrite in RUN : <> < me : User | option: depthFirst, output: empty, input:
     n1999 @ 'additive-normal-form[[empty]] > createInterpreter(
@@ -19,7 +19,7 @@ result Configuration: <> < me : User | option: depthFirst, output: ('__[
     'I.RomanSymbol,'I.RomanSymbol,'I.RomanSymbol,'I.RomanSymbol]), solcount: 1,
     input: '__['M.RomanSymbol,'C.RomanSymbol,'M.RomanSymbol,'X.RomanSymbol,
     'C.RomanSymbol,'I.RomanSymbol,'X.RomanSymbol] @ 'additive-normal-form[[
-    empty]] > noSuchResult(me, interpreter(0), 105)
+    empty]] > noSuchResult(me, interpreter(0), 11)
 ==========================================
 erewrite in RUN : <> < me : User | option: depthFirst, output: empty, input:
     n1999 @ 'add[none]{empty} > createInterpreter(interpreterManager, me, none)
@@ -35,7 +35,7 @@ result Configuration: <> < me : User | option: depthFirst, output: ('__[
     'X.RomanSymbol,'I.RomanSymbol,'X.RomanSymbol]), solcount: 3, input: '__[
     'M.RomanSymbol,'C.RomanSymbol,'M.RomanSymbol,'X.RomanSymbol,'C.RomanSymbol,
     'I.RomanSymbol,'X.RomanSymbol] @ 'add[none]{empty} > noSuchResult(me,
-    interpreter(0), 3)
+    interpreter(0), 0)
 ==========================================
 erewrite in RUN : <> < me : User | option: depthFirst, output: empty, input:
     n1999 @ 'sort[none]{empty} ; 'add[none]{empty} > createInterpreter(
@@ -58,5 +58,5 @@ result Configuration: <> < me : User | option: depthFirst, output: ('__[
     'X.RomanSymbol,'I.RomanSymbol]), solcount: 6, input: '__['M.RomanSymbol,
     'C.RomanSymbol,'M.RomanSymbol,'X.RomanSymbol,'C.RomanSymbol,'I.RomanSymbol,
     'X.RomanSymbol] @ 'sort[none]{empty} ; 'add[none]{empty} > noSuchResult(me,
-    interpreter(0), 64)
+    interpreter(0), 0)
 Bye.
diff --git a/tests/Meta/metaProcStrategy.expected b/tests/Meta/metaProcStrategy.expected
index 6ff74407..7b2e0c83 100644
--- a/tests/Meta/metaProcStrategy.expected
+++ b/tests/Meta/metaProcStrategy.expected
@@ -8,7 +8,7 @@ result Configuration: <> < me : User | option: breadthFirst, output: ('__[
     'I.RomanSymbol,'I.RomanSymbol,'I.RomanSymbol,'I.RomanSymbol]), solcount: 1,
     input: '__['M.RomanSymbol,'C.RomanSymbol,'M.RomanSymbol,'X.RomanSymbol,
     'C.RomanSymbol,'I.RomanSymbol,'X.RomanSymbol] @ 'additive-normal-form[[
-    empty]] > noSuchResult(me, interpreter(0), 105)
+    empty]] > noSuchResult(me, interpreter(0), 0)
 ==========================================
 erewrite in RUN : <> < me : User | option: depthFirst, output: empty, input:
     n1999 @ 'additive-normal-form[[empty]] > createInterpreter(
@@ -19,7 +19,7 @@ result Configuration: <> < me : User | option: depthFirst, output: ('__[
     'I.RomanSymbol,'I.RomanSymbol,'I.RomanSymbol,'I.RomanSymbol]), solcount: 1,
     input: '__['M.RomanSymbol,'C.RomanSymbol,'M.RomanSymbol,'X.RomanSymbol,
     'C.RomanSymbol,'I.RomanSymbol,'X.RomanSymbol] @ 'additive-normal-form[[
-    empty]] > noSuchResult(me, interpreter(0), 105)
+    empty]] > noSuchResult(me, interpreter(0), 11)
 ==========================================
 erewrite in RUN : <> < me : User | option: depthFirst, output: empty, input:
     n1999 @ 'add[none]{empty} > createInterpreter(interpreterManager, me,
@@ -35,7 +35,7 @@ result Configuration: <> < me : User | option: depthFirst, output: ('__[
     'X.RomanSymbol,'I.RomanSymbol,'X.RomanSymbol]), solcount: 3, input: '__[
     'M.RomanSymbol,'C.RomanSymbol,'M.RomanSymbol,'X.RomanSymbol,'C.RomanSymbol,
     'I.RomanSymbol,'X.RomanSymbol] @ 'add[none]{empty} > noSuchResult(me,
-    interpreter(0), 3)
+    interpreter(0), 0)
 ==========================================
 erewrite in RUN : <> < me : User | option: depthFirst, output: empty, input:
     n1999 @ 'sort[none]{empty} ; 'add[none]{empty} > createInterpreter(
@@ -58,5 +58,5 @@ result Configuration: <> < me : User | option: depthFirst, output: ('__[
     'X.RomanSymbol,'I.RomanSymbol]), solcount: 6, input: '__['M.RomanSymbol,
     'C.RomanSymbol,'M.RomanSymbol,'X.RomanSymbol,'C.RomanSymbol,'I.RomanSymbol,
     'X.RomanSymbol] @ 'sort[none]{empty} ; 'add[none]{empty} > noSuchResult(me,
-    interpreter(0), 64)
+    interpreter(0), 0)
 Bye.
diff --git a/tests/ResolvedBugs/Makefile.am b/tests/ResolvedBugs/Makefile.am
index bc7d0364..31531353 100644
--- a/tests/ResolvedBugs/Makefile.am
+++ b/tests/ResolvedBugs/Makefile.am
@@ -63,7 +63,8 @@ TESTS = \
 	pseudoParameterTheoryConstantMarch2023 \
 	redBlackNonLinearApril2023 \
 	redBlackTooFewSubjectsApril2023 \
-	redBlackNGA_April2023
+	redBlackNGA_April2023 \
+	stripperCollectorSwitchMay2023
 
 MAUDE_FILES = \
 	CUIbug12-22-09.maude \
@@ -130,7 +131,8 @@ MAUDE_FILES = \
 	pseudoParameterTheoryConstantMarch2023.maude \
 	redBlackNonLinearApril2023.maude  \
 	redBlackTooFewSubjectsApril2023.maude  \
-	redBlackNGA_April2023.maude 
+	redBlackNGA_April2023.maude \
+	stripperCollectorSwitchMay2023.maude
 
 RESULT_FILES = \
 	CUIbug12-22-09.expected \
@@ -197,6 +199,7 @@ RESULT_FILES = \
 	pseudoParameterTheoryConstantMarch2023.expected \
 	redBlackNonLinearApril2023.expected \
 	redBlackTooFewSubjectsApril2023.expected \
-	redBlackNGA_April2023.expected
+	redBlackNGA_April2023.expected \
+	stripperCollectorSwitchMay2023.expected
 
 EXTRA_DIST = $(TESTS) $(MAUDE_FILES) $(RESULT_FILES)
diff --git a/tests/ResolvedBugs/Makefile.in b/tests/ResolvedBugs/Makefile.in
index 3757f26d..f78c589e 100644
--- a/tests/ResolvedBugs/Makefile.in
+++ b/tests/ResolvedBugs/Makefile.in
@@ -500,7 +500,8 @@ TESTS = \
 	pseudoParameterTheoryConstantMarch2023 \
 	redBlackNonLinearApril2023 \
 	redBlackTooFewSubjectsApril2023 \
-	redBlackNGA_April2023
+	redBlackNGA_April2023 \
+	stripperCollectorSwitchMay2023
 
 MAUDE_FILES = \
 	CUIbug12-22-09.maude \
@@ -567,7 +568,8 @@ MAUDE_FILES = \
 	pseudoParameterTheoryConstantMarch2023.maude \
 	redBlackNonLinearApril2023.maude  \
 	redBlackTooFewSubjectsApril2023.maude  \
-	redBlackNGA_April2023.maude 
+	redBlackNGA_April2023.maude \
+	stripperCollectorSwitchMay2023.maude
 
 RESULT_FILES = \
 	CUIbug12-22-09.expected \
@@ -634,7 +636,8 @@ RESULT_FILES = \
 	pseudoParameterTheoryConstantMarch2023.expected \
 	redBlackNonLinearApril2023.expected \
 	redBlackTooFewSubjectsApril2023.expected \
-	redBlackNGA_April2023.expected
+	redBlackNGA_April2023.expected \
+	stripperCollectorSwitchMay2023.expected
 
 EXTRA_DIST = $(TESTS) $(MAUDE_FILES) $(RESULT_FILES)
 all: all-am
@@ -1273,6 +1276,13 @@ redBlackNGA_April2023.log: redBlackNGA_April2023
 	--log-file $$b.log --trs-file $$b.trs \
 	$(am__common_driver_flags) $(AM_LOG_DRIVER_FLAGS) $(LOG_DRIVER_FLAGS) -- $(LOG_COMPILE) \
 	"$$tst" $(AM_TESTS_FD_REDIRECT)
+stripperCollectorSwitchMay2023.log: stripperCollectorSwitchMay2023
+	@p='stripperCollectorSwitchMay2023'; \
+	b='stripperCollectorSwitchMay2023'; \
+	$(am__check_pre) $(LOG_DRIVER) --test-name "$$f" \
+	--log-file $$b.log --trs-file $$b.trs \
+	$(am__common_driver_flags) $(AM_LOG_DRIVER_FLAGS) $(LOG_DRIVER_FLAGS) -- $(LOG_COMPILE) \
+	"$$tst" $(AM_TESTS_FD_REDIRECT)
 .test.log:
 	@p='$<'; \
 	$(am__set_b); \
diff --git a/tests/ResolvedBugs/stripperCollectorSwitchMay2023 b/tests/ResolvedBugs/stripperCollectorSwitchMay2023
new file mode 100755
index 00000000..a3da519b
--- /dev/null
+++ b/tests/ResolvedBugs/stripperCollectorSwitchMay2023
@@ -0,0 +1,10 @@
+#!/bin/sh
+
+MAUDE_LIB=$srcdir/../../src/Main
+export MAUDE_LIB
+
+../../src/Main/maude \
+  < $srcdir/stripperCollectorSwitchMay2023.maude -no-banner \
+  > stripperCollectorSwitchMay2023.out 2>&1
+
+diff $srcdir/stripperCollectorSwitchMay2023.expected stripperCollectorSwitchMay2023.out > /dev/null 2>&1
diff --git a/tests/ResolvedBugs/stripperCollectorSwitchMay2023.expected b/tests/ResolvedBugs/stripperCollectorSwitchMay2023.expected
new file mode 100644
index 00000000..b1d6d217
--- /dev/null
+++ b/tests/ResolvedBugs/stripperCollectorSwitchMay2023.expected
@@ -0,0 +1,13 @@
+==========================================
+reduce in FOO : h(g(7, z)) .
+rewrites: 8
+result Bool: true
+==========================================
+reduce in FOO : h(g(8, z)) .
+rewrites: 9
+result Bool: true
+==========================================
+reduce in FOO : h(g(20, z)) .
+rewrites: 21
+result Bool: true
+Bye.
diff --git a/tests/ResolvedBugs/stripperCollectorSwitchMay2023.maude b/tests/ResolvedBugs/stripperCollectorSwitchMay2023.maude
new file mode 100644
index 00000000..4e180cb6
--- /dev/null
+++ b/tests/ResolvedBugs/stripperCollectorSwitchMay2023.maude
@@ -0,0 +1,30 @@
+set show timing off .
+
+***
+***	Crafted example to illustrate bug if variables are sorted after the stripper and
+***	collector variables have been determined and they switch places, causing match failure.
+***
+
+fmod FOO is
+  pr NAT .
+  sorts Set Elt .
+  subsort Elt < Set .
+var S : Set .
+var E : Elt .
+var N : Nat .
+  op dummy : Set -> Set .
+  eq dummy(S) = S .
+
+  op z : -> Elt .
+  op p_ : Elt -> Elt .
+  op g : Nat Set -> Set .
+  eq g(s N, E) = f(g(N, p E), E) .
+  
+  op f : Set Set -> Set [assoc comm] .
+  op h : Set -> Bool .
+  ceq h(f(S, E)) = true if E = z .
+endfm
+
+red h(g(7, z)) .
+red h(g(8, z)) .
+red h(g(20, z)) .
diff --git a/tests/StrategyLanguage/metalevel.expected b/tests/StrategyLanguage/metalevel.expected
index 35ff74a1..ccf7e1a4 100644
--- a/tests/StrategyLanguage/metalevel.expected
+++ b/tests/StrategyLanguage/metalevel.expected
@@ -105,12 +105,12 @@ endv
 ==========================================
 reduce in META-LEVEL : metaSrewrite(upModule('SFOO, false), 'a.Foo, 'ac[[
     empty]] | 'ab[none]{empty}, breadthFirst, 0) .
-rewrites: 2
+rewrites: 3
 result ResultPair: {'b.Foo,'Foo}
 ==========================================
 reduce in META-LEVEL : metaSrewrite(['SFOO], 'a.Foo, 'ac[[empty]] | 'ab[none]{
     empty}, breadthFirst, 0) .
-rewrites: 2
+rewrites: 3
 result ResultPair: {'b.Foo,'Foo}
 ==========================================
 reduce in META-LEVEL : metaSrewrite(['SFOO], 'a.Foo, 'ac[[empty]] | 'ab[none]{
@@ -120,7 +120,7 @@ result ResultPair: {'b.Foo,'Foo}
 ==========================================
 reduce in META-LEVEL : metaSrewrite(['SFOO], 'a.Foo, 'ac[[empty]] | 'ab[none]{
     empty}, breadthFirst, 1) .
-rewrites: 2
+rewrites: 4
 result ResultPair: {'c.Foo,'Foo}
 ==========================================
 reduce in META-LEVEL : metaSrewrite(['SFOO], 'a.Foo, 'ac[[empty]] | 'ab[none]{
@@ -130,12 +130,12 @@ result ResultPair?: (failure).ResultPair?
 ==========================================
 reduce in META-LEVEL : metaSrewrite(['SFOO], 'a.Foo, 'ac[[empty]] | 'ab[none]{
     empty}, depthFirst, 1) .
-rewrites: 2
+rewrites: 5
 result ResultPair: {'b.Foo,'Foo}
 ==========================================
 reduce in META-LEVEL : metaSrewrite(['SFOO], 'a.Foo, 'ac[[empty]] | 'ab[none]{
     empty}, depthFirst, 0) .
-rewrites: 2
+rewrites: 4
 result ResultPair: {'c.Foo,'Foo}
 ==========================================
 reduce in META-LEVEL : metaSrewrite(mod 'INC is
@@ -147,7 +147,7 @@ reduce in META-LEVEL : metaSrewrite(mod 'INC is
   none
   rl 'N:Nat => 's_['N:Nat] [label('inc)] .
 endm, '0.Nat, ('inc[none]{empty}) *, breadthFirst, 8) .
-rewrites: 1
+rewrites: 29
 result ResultPair: {'s_^8['0.Zero],'NzNat}
 ==========================================
 reduce in META-LEVEL : metaSrewrite(['SFOO], 'a.Foo, 'bad-rule[none]{empty},