From 7988675ce9666b6f2214b583d42b9fa8be52ae60 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 19 Sep 2019 09:44:04 -0500
Subject: Support context-(in)dependent decision strategies. (#3281)

---
 src/theory/uf/cardinality_extension.cpp | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/theory/uf')

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 94e5f67c1..87696ef5f 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -504,6 +504,8 @@ void SortModel::initialize( OutputChannel* out ){
   if (d_c_dec_strat.get() != nullptr && !d_initialized)
   {
     d_initialized = true;
+    // Strategy is user-context-dependent, since it is in sync with
+    // user-context-dependent flag d_initialized.
     d_thss->getTheory()->getDecisionManager()->registerStrategy(
         DecisionManager::STRAT_UF_CARD, d_c_dec_strat.get());
   }
-- 
cgit v1.2.3