diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 8c9510055..ea21bc329 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -281,6 +281,9 @@ namespace smt {
             ast_manager& m = get_manager();
             if (!m_cuber) {
                 m_cuber = alloc(cuber, *this);
+                // force propagation
+                push_core();
+                pop_core(1);
             }
             expr_ref result = m_cuber->cube();
             expr_ref_vector lits(m);
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 763e0467c..4339e45aa 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -264,7 +264,8 @@ public:
     }
 
     expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override {
-        return m_solver1->cube(vars, backtrack_level);
+        switch_inc_mode();
+        return m_solver2->cube(vars, backtrack_level);
     }
 
     expr * get_assumption(unsigned idx) const override {
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 0090cc3b0..448adc479 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -80,6 +80,7 @@ public:
 
     expr_ref_vector cube(expr_ref_vector& vars, unsigned ) override {
         set_reason_unknown("cubing is not supported on tactics");
+        IF_VERBOSE(1, verbose_stream() << "cubing is not supported on tactics\n");
         return expr_ref_vector(get_manager());
     }