mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Leonardo de Moura 2013-06-28 19:21:34 -07:00
parent d9941c0ccc 9dfd202fdb
commit b7c2d9054b
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -218,7 +218,7 @@ protected:
else if (m.is_bool(arg)) { else if (m.is_bool(arg)) {
res = local_simplify(a, n, id, i); res = local_simplify(a, n, id, i);
TRACE("ctx_solver_simplify_tactic", TRACE("ctx_solver_simplify_tactic",
tout << "Already cached: " << path_r.first << " " << mk_pp(res, m) << "\n";); tout << "Already cached: " << path_r.first << " " << mk_pp(arg, m) << " |-> " << mk_pp(res, m) << "\n";);
args.push_back(res); args.push_back(res);
} }
else { else {
@ -327,7 +327,7 @@ protected:
tmp = m.mk_eq(result, n); tmp = m.mk_eq(result, n);
m_solver.assert_expr(tmp); m_solver.assert_expr(tmp);
if (!simplify_bool(n2, result)) { if (!simplify_bool(n2, result)) {
result = a; result = a->get_arg(index);
} }
m_solver.pop(1); m_solver.pop(1);
return result; return result;

4
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -2437,7 +2437,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
t = m_bv_util.mk_bv_sub(t, lz); t = m_bv_util.mk_bv_sub(t, lz);
t = m_bv_util.mk_bv_sub(t, m_bv_util.mk_sign_extend(2, e_min)); t = m_bv_util.mk_bv_sub(t, m_bv_util.mk_sign_extend(2, e_min));
expr_ref TINY(m); expr_ref TINY(m);
TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral(-1, ebits+2)); TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral((unsigned)-1, ebits+2));
TRACE("fpa2bv_dbg", tout << "TINY = " << mk_ismt2_pp(TINY, m) << std::endl;); TRACE("fpa2bv_dbg", tout << "TINY = " << mk_ismt2_pp(TINY, m) << std::endl;);
SASSERT(is_well_sorted(m, TINY)); SASSERT(is_well_sorted(m, TINY));
@ -2481,7 +2481,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
m_simp.mk_ite(sigma_le_cap, sigma_neg, sigma_cap, sigma_neg_capped); m_simp.mk_ite(sigma_le_cap, sigma_neg, sigma_cap, sigma_neg_capped);
dbg_decouple("fpa2bv_rnd_sigma_neg", sigma_neg); dbg_decouple("fpa2bv_rnd_sigma_neg", sigma_neg);
dbg_decouple("fpa2bv_rnd_sigma_neg_capped", sigma_neg_capped); dbg_decouple("fpa2bv_rnd_sigma_neg_capped", sigma_neg_capped);
sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral(-1, sigma_size)); sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral((unsigned)-1, sigma_size));
dbg_decouple("fpa2bv_rnd_sigma_lt_zero", sigma_lt_zero); dbg_decouple("fpa2bv_rnd_sigma_lt_zero", sigma_lt_zero);
sig_ext = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_size)); sig_ext = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_size));