diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index ada6be1bf..95f531a10 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -1158,7 +1158,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
         result = m().mk_ite(m().mk_eq(arg1, m_util.mk_real(0)),
                             m_util.mk_real(1),
                             result);
-        return BR_REWRITE2;
+        return BR_REWRITE3;
     }
 
     if (!is_int_sort && is_num_y && !y.is_int() && !numerator(y).is_one()) {
diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index 3757b8b55..d7658ca17 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -273,6 +273,7 @@ lia_move int_solver::find_cube() {
     _sp.pop();
     m_lar_solver->round_to_integer_solution();
     settings().st().m_cube_success++;
+    TRACE("cube", tout << "sat with cube\n";);
     return lia_move::sat;
 }