From a319f4bf588af7c556b92fd73077c0ec9b68cdf3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Mar 2020 05:16:48 -0800 Subject: [PATCH] fix #3104 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 2 +- src/tactic/core/solve_eqs_tactic.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 ebe39b2cd..08ad077df 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1130,7 +1130,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res result = m_util.mk_power(m_util.mk_div(m_util.mk_numeral(rational(1), false), arg1), m_util.mk_numeral(-y, false)); result = m().mk_ite(m().mk_eq(arg1, m_util.mk_real(0)), - m_util.mk_real(1), + m_util.mk_real(0), result); return BR_REWRITE3; } diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index d474214c2..f639ca607 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -1007,6 +1007,7 @@ class solve_eqs_tactic : public tactic { SASSERT(g->is_well_sorted()); model_converter_ref mc; tactic_report report("solve_eqs", *g); + TRACE("solve_eqs", g->display(tout);); m_produce_models = g->models_enabled(); m_produce_proofs = g->proofs_enabled(); m_produce_unsat_cores = g->unsat_core_enabled();