Guard relevant domain computation properly, minor. (#1325)

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 67930ce2b6d4c0136a90c3e3662b981c09f9d076..3bd1ac4952329ddf4676735e8507dda2d5282005 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -129,16 +129,15 @@ bool InstStrategyEnum::process(Node f, bool fullEffort)
       {
         Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..."
                           << std::endl;
+        Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl;
+        rd->compute();
+        Trace("inst-alg-debug") << "...finished" << std::endl;
       }
       else
       {
         Trace("inst-alg") << "-> Ground term instantiate " << f << "..."
                           << std::endl;
       }
-      AlwaysAssert(rd);
-      Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl;
-      rd->compute();
-      Trace("inst-alg-debug") << "...finished" << std::endl;
       unsigned final_max_i = 0;
       std::vector<unsigned> maxs;
       std::vector<bool> max_zero;
@@ -170,11 +169,11 @@ bool InstStrategyEnum::process(Node f, bool fullEffort)
               if (!options::cbqi()
                   || !quantifiers::TermUtil::hasInstConstAttr(gt))
               {
-                Node r =
+                Node rep =
                     d_quantEngine->getEqualityQuery()->getRepresentative(gt);
-                if (reps_found.find(r) == reps_found.end())
+                if (reps_found.find(rep) == reps_found.end())
                 {
-                  reps_found[r] = gt;
+                  reps_found[rep] = gt;
                   term_db_list[tn].push_back(gt);
                 }
               }