diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp
index d924f36d7..2814fc249 100644
--- a/src/muz/spacer/spacer_iuc_solver.cpp
+++ b/src/muz/spacer/spacer_iuc_solver.cpp
@@ -127,6 +127,28 @@ lbool iuc_solver::check_sat (unsigned num_assumptions, expr * const *assumptions
     return res;
 }
 
+lbool iuc_solver::check_sat_cc(const expr_ref_vector &cube,
+                               const expr_ref_vector &clause) {
+    if (clause.empty()) {return check_sat(cube.size(), cube.c_ptr());}
+
+    // -- remove any old assumptions
+    if (m_assumptions.size() > m_first_assumption)
+    { m_assumptions.shrink(m_first_assumption); }
+
+    // -- replace theory literals in background assumptions with proxies
+    mk_proxies(m_assumptions);
+    // -- in case mk_proxies added new literals, they are all background
+    m_first_assumption = m_assumptions.size();
+
+    m_assumptions.append(cube);
+    m_is_proxied = mk_proxies(m_assumptions, m_first_assumption);
+
+    lbool res;
+    res = m_solver.check_sat_cc(m_assumptions, clause);
+    set_status (res);
+    return res;
+}
+
 
 app* iuc_solver::def_manager::mk_proxy (expr *v)
 {
diff --git a/src/muz/spacer/spacer_iuc_solver.h b/src/muz/spacer/spacer_iuc_solver.h
index 8bb0a8605..72d995208 100644
--- a/src/muz/spacer/spacer_iuc_solver.h
+++ b/src/muz/spacer/spacer_iuc_solver.h
@@ -123,6 +123,7 @@ public:
     {return m_solver.get_scope_level();}
 
     lbool check_sat(unsigned num_assumptions, expr * const *assumptions) override;
+    lbool check_sat_cc(const expr_ref_vector &cube, const expr_ref_vector &clause) override;
     void set_progress_callback(progress_callback *callback) override
     {m_solver.set_progress_callback(callback);}
     unsigned get_num_assertions() const override