Merge branch 'master' into m1buildm1build

17 files changed, 179 insertions, 214 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index d439f33a6..5b65951a6 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -22,86 +22,37 @@
 namespace cvc5 {
 namespace decision {
 
-DecisionEngine::DecisionEngine(context::Context* c,
-                               context::UserContext* u,
-                               prop::SkolemDefManager* skdm,
-                               ResourceManager* rm)
-    : d_decEngineOld(new DecisionEngineOld(c, u)),
-      d_jstrat(new JustificationStrategy(c, u, skdm)),
+DecisionEngine::DecisionEngine(context::Context* c, ResourceManager* rm)
+    : d_context(c),
       d_resourceManager(rm),
-      d_useOld(options::decisionMode() != options::DecisionMode::JUSTIFICATION)
+      d_cnfStream(nullptr),
+      d_satSolver(nullptr)
 {
 }
 
-void DecisionEngine::finishInit(prop::CDCLTSatSolverInterface* ss,
-                                prop::CnfStream* cs)
+void DecisionEngine::finishInit(CDCLTSatSolverInterface* ss, CnfStream* cs)
 {
-  if (d_useOld)
-  {
-    d_decEngineOld->setSatSolver(ss);
-    d_decEngineOld->setCnfStream(cs);
-    return;
-  }
-  d_jstrat->finishInit(ss, cs);
-}
-
-void DecisionEngine::presolve()
-{
-  if (!d_useOld)
-  {
-    d_jstrat->presolve();
-  }
+  d_satSolver = ss;
+  d_cnfStream = cs;
 }
 
 prop::SatLiteral DecisionEngine::getNext(bool& stopSearch)
 {
   d_resourceManager->spendResource(Resource::DecisionStep);
-  if (d_useOld)
-  {
-    return d_decEngineOld->getNext(stopSearch);
-  }
-  return d_jstrat->getNext(stopSearch);
-}
-
-bool DecisionEngine::isDone()
-{
-  if (d_useOld)
-  {
-    return d_decEngineOld->isDone();
-  }
-  return d_jstrat->isDone();
+  return getNextInternal(stopSearch);
 }
 
-void DecisionEngine::addAssertion(TNode assertion)
+DecisionEngineEmpty::DecisionEngineEmpty(context::Context* sc,
+                                         ResourceManager* rm)
+    : DecisionEngine(sc, rm)
 {
-  if (d_useOld)
-  {
-    d_decEngineOld->addAssertion(assertion);
-    return;
-  }
-  d_jstrat->addAssertion(assertion);
 }
-
-void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem)
-{
-  if (d_useOld)
-  {
-    d_decEngineOld->addSkolemDefinition(lem, skolem);
-  }
-  else
-  {
-    d_jstrat->addSkolemDefinition(lem, skolem);
-  }
-}
-
-void DecisionEngine::notifyAsserted(TNode n)
+bool DecisionEngineEmpty::isDone() { return false; }
+void DecisionEngineEmpty::addAssertion(TNode assertion) {}
+void DecisionEngineEmpty::addSkolemDefinition(TNode lem, TNode skolem) {}
+prop::SatLiteral DecisionEngineEmpty::getNextInternal(bool& stopSearch)
 {
-  if (d_useOld)
-  {
-    return;
-  }
-  // old implementation does not use this
-  d_jstrat->notifyAsserted(n);
+  return undefSatLiteral;
 }
 
 }  // namespace decision
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index e54e1fc3c..4cf057840 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -18,20 +18,12 @@
 #ifndef CVC5__DECISION__DECISION_ENGINE_H
 #define CVC5__DECISION__DECISION_ENGINE_H
 
-#include "decision/justification_strategy.h"
 #include "expr/node.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_types.h"
 
 namespace cvc5 {
-
-namespace prop {
-class SkolemDefManager;
-}
-
-class DecisionEngineOld;
-
 namespace decision {
 
 class DecisionEngine
@@ -39,48 +31,68 @@ class DecisionEngine
  public:
   /** Constructor */
   DecisionEngine(context::Context* sc,
-                 context::UserContext* uc,
-                 prop::SkolemDefManager* skdm,
                  ResourceManager* rm);
+  virtual ~DecisionEngine() {}
 
   /** Finish initialize */
   void finishInit(prop::CDCLTSatSolverInterface* ss, prop::CnfStream* cs);
 
   /** Presolve, called at the beginning of each check-sat call */
-  void presolve();
+  virtual void presolve() {}
 
-  /** Gets the next decision based on strategies that are enabled */
+  /**
+   * Gets the next decision based on strategies that are enabled. This sets
+   * stopSearch to true if no further SAT variables need to be assigned in
+   * this SAT context.
+   */
   prop::SatLiteral getNext(bool& stopSearch);
 
   /** Is the DecisionEngine in a state where it has solved everything? */
-  bool isDone();
+  virtual bool isDone() = 0;
 
   /**
    * Notify this class that assertion is an (input) assertion, not corresponding
    * to a skolem definition.
    */
-  void addAssertion(TNode assertion);
+  virtual void addAssertion(TNode assertion) = 0;
   /**
-   * !!!! temporary until the old justification implementation is deleted.
-   * Notify this class  that lem is the skolem definition for skolem, which is
+   * Notify this class that lem is the skolem definition for skolem, which is
    * a part of the current assertions.
    */
-  void addSkolemDefinition(TNode lem, TNode skolem);
+  virtual void addSkolemDefinition(TNode lem, TNode skolem) = 0;
   /**
    * Notify this class that the literal n has been asserted, possibly
    * propagated by the SAT solver.
    */
-  void notifyAsserted(TNode n);
+  virtual void notifyAsserted(TNode n) {}
 
- private:
-  /** The old implementation */
-  std::unique_ptr<DecisionEngineOld> d_decEngineOld;
-  /** The new implementation */
-  std::unique_ptr<JustificationStrategy> d_jstrat;
+ protected:
+  /** Get next internal, the engine-specific implementation of getNext */
+  virtual prop::SatLiteral getNextInternal(bool& stopSearch) = 0;
+  /** Pointer to the SAT context */
+  context::Context* d_context;
   /** Pointer to resource manager for associated SmtEngine */
   ResourceManager* d_resourceManager;
-  /** using old implementation? */
-  bool d_useOld;
+  /** Pointer to the CNF stream */
+  prop::CnfStream* d_cnfStream;
+  /** Pointer to the SAT solver */
+  prop::CDCLTSatSolverInterface* d_satSolver;
+};
+
+/**
+ * Instance of the above class which does nothing. This is used when
+ * the decision mode is set to internal.
+ */
+class DecisionEngineEmpty : public DecisionEngine
+{
+ public:
+  DecisionEngineEmpty(context::Context* sc, ResourceManager* rm);
+  bool isDone() override;
+  void addAssertion(TNode assertion) override;
+  void addSkolemDefinition(TNode lem, TNode skolem) override;
+
+ protected:
+  prop::SatLiteral getNextInternal(bool& stopSearch) override;
 };
 
 }  // namespace decision
diff --git a/src/decision/decision_engine_old.cpp b/src/decision/decision_engine_old.cpp
index 8ef7ad1f4..6bfba35ee 100644
--- a/src/decision/decision_engine_old.cpp
+++ b/src/decision/decision_engine_old.cpp
@@ -26,14 +26,14 @@ using namespace std;
 namespace cvc5 {
 
 DecisionEngineOld::DecisionEngineOld(context::Context* sc,
-                                     context::UserContext* uc)
-    : d_cnfStream(nullptr),
-      d_satSolver(nullptr),
-      d_satContext(sc),
-      d_userContext(uc),
+                                     context::UserContext* uc,
+                                     ResourceManager* rm)
+    : DecisionEngine(sc, rm),
       d_result(sc, SAT_VALUE_UNKNOWN),
       d_engineState(0),
-      d_enabledITEStrategy(nullptr)
+      d_enabledITEStrategy(nullptr),
+      d_decisionStopOnly(options::decisionMode()
+                         == options::DecisionMode::STOPONLY_OLD)
 {
   Trace("decision") << "Creating decision engine" << std::endl;
   Assert(d_engineState == 0);
@@ -42,13 +42,13 @@ DecisionEngineOld::DecisionEngineOld(context::Context* sc,
   Trace("decision-init") << "DecisionEngineOld::init()" << std::endl;
   Trace("decision-init") << " * options->decisionMode: "
                          << options::decisionMode() << std::endl;
-  Trace("decision-init") << " * options->decisionStopOnly: "
-                         << options::decisionStopOnly() << std::endl;
+  Trace("decision-init") << " * decisionStopOnly: " << d_decisionStopOnly
+                         << std::endl;
 
   if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
   {
-    d_enabledITEStrategy.reset(new decision::JustificationHeuristic(
-        this, d_userContext, d_satContext));
+    d_enabledITEStrategy.reset(
+        new decision::JustificationHeuristic(this, uc, sc));
   }
 }
 
@@ -61,16 +61,18 @@ void DecisionEngineOld::shutdown()
   d_enabledITEStrategy.reset(nullptr);
 }
 
-SatLiteral DecisionEngineOld::getNext(bool& stopSearch)
+SatLiteral DecisionEngineOld::getNextInternal(bool& stopSearch)
 {
   Assert(d_cnfStream != nullptr)
       << "Forgot to set cnfStream for decision engine?";
   Assert(d_satSolver != nullptr)
       << "Forgot to set satSolver for decision engine?";
 
-  return d_enabledITEStrategy == nullptr
-             ? undefSatLiteral
-             : d_enabledITEStrategy->getNext(stopSearch);
+  SatLiteral ret = d_enabledITEStrategy == nullptr
+                       ? undefSatLiteral
+                       : d_enabledITEStrategy->getNext(stopSearch);
+  // if we are doing stop only, we don't return the literal
+  return d_decisionStopOnly ? undefSatLiteral : ret;
 }
 
 void DecisionEngineOld::addAssertion(TNode assertion)
diff --git a/src/decision/decision_engine_old.h b/src/decision/decision_engine_old.h
index 4e7bde4b5..3e9a563b7 100644
--- a/src/decision/decision_engine_old.h
+++ b/src/decision/decision_engine_old.h
@@ -20,6 +20,7 @@
 
 #include "base/output.h"
 #include "context/cdo.h"
+#include "decision/decision_engine.h"
 #include "decision/decision_strategy.h"
 #include "expr/node.h"
 #include "prop/cnf_stream.h"
@@ -32,13 +33,15 @@ using namespace cvc5::decision;
 
 namespace cvc5 {
 
-class DecisionEngineOld
+class DecisionEngineOld : public decision::DecisionEngine
 {
  public:
   // Necessary functions
 
   /** Constructor */
-  DecisionEngineOld(context::Context* sc, context::UserContext* uc);
+  DecisionEngineOld(context::Context* sc,
+                    context::UserContext* uc,
+                    ResourceManager* rm);
 
   /** Destructor, currently does nothing */
   ~DecisionEngineOld()
@@ -46,22 +49,6 @@ class DecisionEngineOld
     Trace("decision") << "Destroying decision engine" << std::endl;
   }
 
-  void setSatSolver(CDCLTSatSolverInterface* ss)
-  {
-    // setPropEngine should not be called more than once
-    Assert(d_satSolver == NULL);
-    Assert(ss != NULL);
-    d_satSolver = ss;
-  }
-
-  void setCnfStream(CnfStream* cs)
-  {
-    // setPropEngine should not be called more than once
-    Assert(d_cnfStream == NULL);
-    Assert(cs != NULL);
-    d_cnfStream = cs;
-  }
-
   /**
    * This is called by SmtEngine, at shutdown time, just before
    * destruction.  It is important because there are destruction
@@ -72,10 +59,10 @@ class DecisionEngineOld
   // Interface for External World to use our services
 
   /** Gets the next decision based on strategies that are enabled */
-  SatLiteral getNext(bool& stopSearch);
+  SatLiteral getNextInternal(bool& stopSearch) override;
 
   /** Is the DecisionEngineOld in a state where it has solved everything? */
-  bool isDone()
+  bool isDone() override
   {
     Trace("decision") << "DecisionEngineOld::isDone() returning "
                       << (d_result != SAT_VALUE_UNKNOWN)
@@ -107,12 +94,12 @@ class DecisionEngineOld
    * Notify this class that assertion is an (input) assertion, not corresponding
    * to a skolem definition.
    */
-  void addAssertion(TNode assertion);
+  void addAssertion(TNode assertion) override;
   /**
    * Notify this class  that lem is the skolem definition for skolem, which is
    * a part of the current assertions.
    */
-  void addSkolemDefinition(TNode lem, TNode skolem);
+  void addSkolemDefinition(TNode lem, TNode skolem) override;
 
   // Interface for Strategies to use stuff stored in Decision Engine
   // (which was possibly requested by them on initialization)
@@ -129,12 +116,6 @@ class DecisionEngineOld
   // Disable creating decision engine without required parameters
   DecisionEngineOld();
 
-  CnfStream* d_cnfStream;
-  CDCLTSatSolverInterface* d_satSolver;
-
-  context::Context* d_satContext;
-  context::UserContext* d_userContext;
-
   // Does decision engine know the answer?
   context::CDO<SatValue> d_result;
 
@@ -142,6 +123,8 @@ class DecisionEngineOld
   unsigned d_engineState;  // 0=pre-init; 1=init,pre-shutdown; 2=shutdown
   /** The ITE decision strategy we have allocated */
   std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy;
+  /** Whether we are using stop only */
+  bool d_decisionStopOnly;
 
 }; /* DecisionEngineOld class */
 
diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp
index b73b24bd0..56d96b32f 100644
--- a/src/decision/justification_strategy.cpp
+++ b/src/decision/justification_strategy.cpp
@@ -25,10 +25,9 @@ namespace decision {
 
 JustificationStrategy::JustificationStrategy(context::Context* c,
                                              context::UserContext* u,
-                                             prop::SkolemDefManager* skdm)
-    : d_context(c),
-      d_cnfStream(nullptr),
-      d_satSolver(nullptr),
+                                             prop::SkolemDefManager* skdm,
+                                             ResourceManager* rm)
+    : DecisionEngine(c, rm),
       d_skdm(skdm),
       d_assertions(
           u,
@@ -40,18 +39,13 @@ JustificationStrategy::JustificationStrategy(context::Context* c,
       d_lastDecisionLit(c),
       d_currStatusDec(false),
       d_useRlvOrder(options::jhRlvOrder()),
+      d_decisionStopOnly(options::decisionMode()
+                         == options::DecisionMode::STOPONLY),
       d_jhSkMode(options::jhSkolemMode()),
       d_jhSkRlvMode(options::jhSkolemRlvMode())
 {
 }
 
-void JustificationStrategy::finishInit(CDCLTSatSolverInterface* ss,
-                                       CnfStream* cs)
-{
-  d_satSolver = ss;
-  d_cnfStream = cs;
-}
-
 void JustificationStrategy::presolve()
 {
   d_lastDecisionLit = Node::null();
@@ -64,7 +58,7 @@ void JustificationStrategy::presolve()
   d_stack.clear();
 }
 
-SatLiteral JustificationStrategy::getNext(bool& stopSearch)
+SatLiteral JustificationStrategy::getNextInternal(bool& stopSearch)
 {
   // ensure we have an assertion
   if (!refreshCurrentAssertion())
@@ -186,6 +180,11 @@ SatLiteral JustificationStrategy::getNext(bool& stopSearch)
           d_lastDecisionLit = next.first;
           // record that we made a decision
           d_currStatusDec = true;
+          if (d_decisionStopOnly)
+          {
+            // only doing stop-only, return undefSatLiteral.
+            return undefSatLiteral;
+          }
           return lastChildVal == SAT_VALUE_FALSE ? ~nsl : nsl;
         }
         else
diff --git a/src/decision/justification_strategy.h b/src/decision/justification_strategy.h
index 667f53115..fc31805dd 100644
--- a/src/decision/justification_strategy.h
+++ b/src/decision/justification_strategy.h
@@ -21,6 +21,7 @@
 #include "context/cdinsert_hashmap.h"
 #include "context/cdo.h"
 #include "decision/assertion_list.h"
+#include "decision/decision_engine.h"
 #include "decision/justify_info.h"
 #include "decision/justify_stack.h"
 #include "decision/justify_stats.h"
@@ -117,19 +118,17 @@ namespace decision {
  * definition, and Q alone would have sufficed to show the input formula
  * was satisfied.
  */
-class JustificationStrategy
+class JustificationStrategy : public DecisionEngine
 {
  public:
   /** Constructor */
   JustificationStrategy(context::Context* c,
                         context::UserContext* u,
-                        prop::SkolemDefManager* skdm);
-
-  /** Finish initialize */
-  void finishInit(prop::CDCLTSatSolverInterface* ss, prop::CnfStream* cs);
+                        prop::SkolemDefManager* skdm,
+                        ResourceManager* rm);
 
   /** Presolve, called at the beginning of each check-sat call */
-  void presolve();
+  void presolve() override;
 
   /**
    * Gets the next decision based on the current assertion to satisfy. This
@@ -140,7 +139,7 @@ class JustificationStrategy
    * @param stopSearch Set to true if we can stop the search
    * @return The next SAT literal to decide on.
    */
-  prop::SatLiteral getNext(bool& stopSearch);
+  prop::SatLiteral getNextInternal(bool& stopSearch) override;
 
   /**
    * Are we finished assigning values to literals?
@@ -148,24 +147,24 @@ class JustificationStrategy
    * @return true if and only if all relevant input assertions are already
    * propositionally satisfied by the current assignment.
    */
-  bool isDone();
+  bool isDone() override;
 
   /**
    * Notify this class that assertion is an (input) assertion, not corresponding
    * to a skolem definition.
    */
-  void addAssertion(TNode assertion);
+  void addAssertion(TNode assertion) override;
   /**
    * Notify this class that lem is the skolem definition for skolem, which is
    * a part of the current assertions.
    */
-  void addSkolemDefinition(TNode lem, TNode skolem);
+  void addSkolemDefinition(TNode lem, TNode skolem) override;
   /**
    * Notify this class that literal n has been asserted. This is triggered when
    * n is sent to TheoryEngine. This activates skolem definitions for skolems
    * k that occur in n.
    */
-  void notifyAsserted(TNode n);
+  void notifyAsserted(TNode n) override;
 
  private:
   /**
@@ -225,12 +224,6 @@ class JustificationStrategy
   static bool isTheoryLiteral(TNode n);
   /** Is n a theory atom? */
   static bool isTheoryAtom(TNode n);
-  /** Pointer to the SAT context */
-  context::Context* d_context;
-  /** Pointer to the CNF stream */
-  prop::CnfStream* d_cnfStream;
-  /** Pointer to the SAT solver */
-  prop::CDCLTSatSolverInterface* d_satSolver;
   /** Pointer to the skolem definition manager */
   prop::SkolemDefManager* d_skdm;
   /** The assertions, which are user-context dependent. */
@@ -252,6 +245,8 @@ class JustificationStrategy
   //------------------------------------ options
   /** using relevancy order */
   bool d_useRlvOrder;
+  /** using stop only */
+  bool d_decisionStopOnly;
   /** skolem mode */
   options::JutificationSkolemMode d_jhSkMode;
   /** skolem relevancy mode */
diff --git a/src/options/README.md b/src/options/README.md
index df5686abc..b0b026166 100644
--- a/src/options/README.md
+++ b/src/options/README.md
@@ -194,14 +194,14 @@ Full Example
     [[option.mode.JUSTIFICATION]]
       name = "justification"
       help = "An ATGP-inspired justification heuristic."
-    [[option.mode.RELEVANCY]]
+    [[option.mode.STOPONLY]]
       name = "justification-stoponly"
       help = "Use the justification heuristic only to stop early, not for decisions."
 
 This defines a new option that is accessible via
 `d_options.{module.id}.decisionMode` and stores an automatically generated mode
 `DecisionMode`, an enum class with the values `INTERNAL`, `JUSTIFICATION` and
-`RELEVANCY`. From the outside, it can be set by `--decision=internal`, but also
+`STOPONLY`. From the outside, it can be set by `--decision=internal`, but also
 with `--decision-mode=justification`, and similarly from an SMT-LIB input with
 `(set-option :decision internal)` and `(set-option :decision-mode
 justification)`. The command-line help for this option looks as follows:
diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml
index 8cc2bf2fe..abb27ac9f 100644
--- a/src/options/decision_options.toml
+++ b/src/options/decision_options.toml
@@ -8,7 +8,6 @@ name   = "Decision Heuristics"
   long       = "decision=MODE"
   type       = "DecisionMode"
   default    = "INTERNAL"
-  predicates = ["setDecisionModeStopOnly"]
   help       = "choose decision mode, see --decision=help"
   help_mode  = "Decision modes."
 [[option.mode.INTERNAL]]
@@ -17,17 +16,15 @@ name   = "Decision Heuristics"
 [[option.mode.JUSTIFICATION]]
   name = "justification"
   help = "An ATGP-inspired justification heuristic."
+[[option.mode.STOPONLY]]
+  name = "stoponly"
+  help = "Use the justification heuristic only to stop early, not for decisions."
 [[option.mode.JUSTIFICATION_OLD]]
   name = "justification-old"
   help = "Older implementation of an ATGP-inspired justification heuristic."
-[[option.mode.RELEVANCY]]
-  name = "justification-stoponly"
-  help = "Use the justification heuristic only to stop early, not for decisions."
-
-[[option]]
-  name       = "decisionStopOnly"
-  category   = "undocumented"
-  type       = "bool"
+[[option.mode.STOPONLY_OLD]]
+  name = "stoponly-old"
+  help = "Use the old implementation of justification heuristic only to stop early, not for decisions."
 
 [[option]]
   name       = "decisionThreshold"
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 6958dcb12..e423dc149 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -234,14 +234,6 @@ InstFormatMode OptionsHandler::stringToInstFormatMode(const std::string& option,
   }
 }
 
-// decision/options_handlers.h
-void OptionsHandler::setDecisionModeStopOnly(const std::string& option,
-                                             const std::string& flag,
-                                             DecisionMode m)
-{
-  d_options->decision.decisionStopOnly = (m == DecisionMode::RELEVANCY);
-}
-
 void OptionsHandler::setProduceAssertions(const std::string& option,
                                           const std::string& flag,
                                           bool value)
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index bf07729ae..eed361c0d 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -100,11 +100,6 @@ public:
                                         const std::string& flag,
                                         const std::string& optarg);
 
-  // decision/options_handlers.h
-  void setDecisionModeStopOnly(const std::string& option,
-                               const std::string& flag,
-                               DecisionMode m);
-
   /**
    * Throws a ModalException if this option is being set after final
    * initialization.
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 62b2f655c..24b98577f 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -21,8 +21,8 @@
 
 #include "base/check.h"
 #include "base/output.h"
-#include "decision/decision_engine.h"
 #include "decision/decision_engine_old.h"
+#include "decision/justification_strategy.h"
 #include "options/base_options.h"
 #include "options/decision_options.h"
 #include "options/main_options.h"
@@ -88,8 +88,22 @@ PropEngine::PropEngine(TheoryEngine* te,
   context::UserContext* userContext = d_env.getUserContext();
   ResourceManager* rm = d_env.getResourceManager();
 
-  d_decisionEngine.reset(
-      new decision::DecisionEngine(satContext, userContext, d_skdm.get(), rm));
+  options::DecisionMode dmode = options::decisionMode();
+  if (dmode == options::DecisionMode::JUSTIFICATION
+      || dmode == options::DecisionMode::STOPONLY)
+  {
+    d_decisionEngine.reset(new decision::JustificationStrategy(
+        satContext, userContext, d_skdm.get(), rm));
+  }
+  else if (dmode == options::DecisionMode::JUSTIFICATION_OLD
+           || dmode == options::DecisionMode::STOPONLY_OLD)
+  {
+    d_decisionEngine.reset(new DecisionEngineOld(satContext, userContext, rm));
+  }
+  else
+  {
+    d_decisionEngine.reset(new decision::DecisionEngineEmpty(satContext, rm));
+  }
 
   d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry());
 
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 845289841..47263af97 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -151,7 +151,7 @@ SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) {
   if(stopSearch) {
     Trace("decision") << "  ***  Decision Engine stopped search *** " << std::endl;
   }
-  return options::decisionStopOnly() ? undefSatLiteral : ret;
+  return ret;
 }
 
 bool TheoryProxy::theoryNeedCheck() const {
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 229fdeec5..f4d885f4b 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -946,9 +946,20 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                       ? true
                       : false);
 
-    Trace("smt") << "setting decision mode to " << decMode << std::endl;
     opts.decision.decisionMode = decMode;
-    opts.decision.decisionStopOnly = stoponly;
+    if (stoponly)
+    {
+      if (opts.decision.decisionMode == options::DecisionMode::JUSTIFICATION)
+      {
+        opts.decision.decisionMode = options::DecisionMode::STOPONLY;
+      }
+      else
+      {
+        Assert(opts.decision.decisionMode == options::DecisionMode::INTERNAL);
+      }
+    }
+    Trace("smt") << "setting decision mode to " << opts.decision.decisionMode
+                 << std::endl;
   }
   if (options::incrementalSolving())
   {
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 063c440a5..62dedb35a 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -305,7 +305,7 @@ void CardinalityExtension::checkCardCycles()
   // build order of equivalence classes, also build cardinality graph
   const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
   d_oSetEqc.clear();
-  d_card_parent.clear();
+  d_cardParent.clear();
   for (const Node& s : setEqc)
   {
     std::vector<Node> curr;
@@ -317,7 +317,6 @@ void CardinalityExtension::checkCardCycles()
     }
   }
 
-  Trace("sets") << "d_card_parent: " << d_card_parent << std::endl;
   Trace("sets") << "d_oSetEqc: " << d_oSetEqc << std::endl;
   Trace("sets") << "Done check cardinality cycles" << std::endl;
 }
@@ -432,14 +431,6 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
       {
         return;
       }
-      else
-      {
-        // justify why there is no edge to parents (necessary?)
-        for (unsigned e = 0; e < n_parents; e++)
-        {
-          Node p = (e == true_sib) ? u : n[e];
-        }
-      }
       continue;
     }
     std::vector<Node> card_parents;
@@ -521,7 +512,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
         card_parent_ids.push_back(is_union ? 2 : e);
       }
     }
-    Assert(d_card_parent[n].empty());
+    Assert(d_cardParent[n].empty());
     Trace("sets-debug") << "get parent representatives..." << std::endl;
     // for each parent, take their representatives
     for (unsigned k = 0, numcp = card_parents.size(); k < numcp; k++)
@@ -573,9 +564,9 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
       else
       {
         bool dup = false;
-        for (unsigned l = 0, numcpn = d_card_parent[n].size(); l < numcpn; l++)
+        for (unsigned l = 0, numcpn = d_cardParent[n].size(); l < numcpn; l++)
         {
-          Node cpnl = d_card_parent[n][l];
+          Node cpnl = d_cardParent[n][l].first;
           if (eqcc != cpnl)
           {
             continue;
@@ -613,7 +604,13 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
               conc.push_back(cpk.eqNode(n));
             }
           }
-          d_im.assertInference(conc, InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2, cpk.eqNode(cpnl));
+          // use the original term, not the representative.
+          // for example, we conclude T = (union T S) => (intersect T S) = S
+          // here where we do not use the representative of T or (union T S).
+          Node cpnlb = d_cardParent[n][l].second;
+          d_im.assertInference(conc,
+                               InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2,
+                               cpk.eqNode(cpnlb));
           d_im.doPendingLemmas();
           if (d_im.hasSent())
           {
@@ -622,18 +619,18 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
         }
         if (!dup)
         {
-          d_card_parent[n].push_back(eqcc);
+          d_cardParent[n].emplace_back(eqcc, cpk);
         }
       }
     }
     // now recurse on parents (to ensure their normal will be computed after
     // this eqc)
     exp.push_back(eqc.eqNode(n));
-    for (const Node& cpnc : d_card_parent[n])
+    for (const std::pair<Node, Node>& cpnc : d_cardParent[n])
     {
-      Trace("sets-cycle-debug")
-          << "Traverse card parent " << eqc << " -> " << cpnc << std::endl;
-      checkCardCyclesRec(cpnc, curr, exp);
+      Trace("sets-cycle-debug") << "Traverse card parent " << eqc << " -> "
+                                << cpnc.first << std::endl;
+      checkCardCyclesRec(cpnc.first, curr, exp);
       if (d_im.hasSent())
       {
         return;
@@ -897,7 +894,7 @@ void CardinalityExtension::checkNormalForm(Node eqc,
   for (const Node& n : nvsets)
   {
     Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl;
-    if (d_card_parent[n].empty())
+    if (d_cardParent[n].empty())
     {
       // nothing to do
       continue;
@@ -905,8 +902,9 @@ void CardinalityExtension::checkNormalForm(Node eqc,
     Assert(d_localBase.find(n) != d_localBase.end());
     Node cbase = d_localBase[n];
     Trace("sets-nf-debug") << "Card base is " << cbase << std::endl;
-    for (const Node& p : d_card_parent[n])
+    for (const std::pair<Node, Node>& cp : d_cardParent[n])
     {
+      Node p = cp.first;
       Trace("sets-nf-debug") << "Check parent " << p << std::endl;
       if (parents_proc[cbase].find(p) != parents_proc[cbase].end())
       {
diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h
index ce2f29bd5..bddcfaf1b 100644
--- a/src/theory/sets/cardinality_extension.h
+++ b/src/theory/sets/cardinality_extension.h
@@ -357,9 +357,12 @@ class CardinalityExtension
   std::vector<Node> d_oSetEqc;
   /**
    * This maps set terms to the set of representatives of their "parent" sets,
-   * see checkCardCycles.
+   * see checkCardCycles. Parents are stored as a pair of the form
+   *   (r, t)
+   * where t is the parent term and r is the representative of equivalence
+   * class of t.
    */
-  std::map<Node, std::vector<Node> > d_card_parent;
+  std::map<Node, std::vector<std::pair<Node, Node>>> d_cardParent;
   /**
    * Maps equivalence classes + set terms in that equivalence class to their
    * "flat form" (see checkNormalForms).
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ea78096dc..cdc77c980 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2068,6 +2068,7 @@ set(regress_1_tests
   regress1/sets/remove_check_free_31_6.smt2
   regress1/sets/sets-disequal.smt2
   regress1/sets/sets-tuple-poly.cvc
+  regress1/sets/sets-uc-wrong.smt2
   regress1/sets/set-comp-sat.smt2
   regress1/sets/sharingbug.smt2
   regress1/sets/univ-set-uf-elim.smt2
diff --git a/test/regress/regress1/sets/sets-uc-wrong.smt2 b/test/regress/regress1/sets/sets-uc-wrong.smt2
new file mode 100644
index 000000000..e8b768d36
--- /dev/null
+++ b/test/regress/regress1/sets/sets-uc-wrong.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun t () (Set Int))
+(declare-fun s () (Set Int))
+(declare-const v Bool)
+(assert (forall ((q Bool)) (distinct v (subset s t))))
+(assert (= 1 (card t)))
+(check-sat)
+(assert v)
+(check-sat)