From 9c0e350bc4e69a808e2180ade992822e3ec11cc7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Jan 2020 18:50:58 -0800 Subject: [PATCH] rewrite3 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 2 +- src/util/lp/int_solver.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) 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; }