diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp
index c8503b46c..afa768863 100644
--- a/src/sat/card_extension.cpp
+++ b/src/sat/card_extension.cpp
@@ -676,14 +676,6 @@ namespace sat {
             }
             result->add_at_least(c.lit().var(), lits, c.k());
         }
-        for (unsigned i = 0; i < m_var_trail.size(); ++i) {
-            bool_var v = m_var_trail[i];
-            if (v != null_bool_var) {
-                card* c = m_var_infos[v].m_card;
-                card* c2 = m_constraints[c->index()];
-                NOT_IMPLEMENTED_YET();
-            }
-        }
         return result;
     }
 
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 3d36e0b53..8326235d9 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -75,7 +75,7 @@ namespace sat {
     void solver::copy(solver const & src) {
         pop_to_base_level();
         SASSERT(m_mc.empty() && src.m_mc.empty());
-        SASSERT(scope_lvl() == 0);
+        SASSERT(at_search_lvl());
         // create new vars
         if (num_vars() < src.num_vars()) {
             for (bool_var v = num_vars(); v < src.num_vars(); v++) {
@@ -85,8 +85,15 @@ namespace sat {
                 VERIFY(v == mk_var(ext, dvar));
             }
         }
+        //
+        // register the extension before performing assignments.
+        // the assignments may call back into the extension.
+        //
+        if (src.get_extension()) {
+            m_ext = src.get_extension()->copy(this);
+        }
         {
-            unsigned sz = src.scope_lvl() == 0 ? src.m_trail.size() : src.m_scopes[0].m_trail_lim;
+            unsigned sz = scope_lvl() == 0 ? src.m_trail.size() : src.m_scopes[0].m_trail_lim;
             for (unsigned i = 0; i < sz; ++i) {
                 assign(src.m_trail[i], justification());
             }
@@ -125,9 +132,6 @@ namespace sat {
             }
         }
 
-        if (src.get_extension()) {
-            m_ext = src.get_extension()->copy(this);
-        }
         m_user_scope_literals.reset();
         m_user_scope_literals.append(src.m_user_scope_literals);
     }
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 25c823446..e17c9e3bf 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -220,6 +220,7 @@ namespace sat {
         bool is_external(bool_var v) const { return m_external[v] != 0; }
         bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
         unsigned scope_lvl() const { return m_scope_lvl; }
+        bool  at_search_lvl() const { return m_scope_lvl == 0; }
         lbool value(literal l) const { return static_cast<lbool>(m_assignment[l.index()]); }
         lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); }
         unsigned lvl(bool_var v) const { return m_level[v]; }