mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-17 00:32:16 +00:00
Code Activity

Fixed side conditions for UFs translated from FP to BV. Fixes #1825.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2018-10-01 15:20:00 +01:00
parent 35bf63d563
commit 2a92de0aee
No known key found for this signature in database
GPG key ID: BCF6360F86294467
3 changed files with 50 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/ast/fpa/fpa2bv_rewriter.cpp
View file

@ -215,6 +215,12 @@ bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q,
new_decl_names.push_back(symbol(name_buffer.c_str()));
new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits));
}
else if (m_conv.is_rm(s)) {
name_buffer.reset();
name_buffer << n << ".bv";
new_decl_names.push_back(symbol(name_buffer.c_str()));
new_decl_sorts.push_back(m_conv.bu().mk_sort(3));
}
else {
new_decl_sorts.push_back(s);
new_decl_names.push_back(n);
@ -248,6 +254,11 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res
m_conv.bu().mk_extract(ebits - 1, 0, new_var),
m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var));
}
else if (m_conv.is_rm(s)) {
expr_ref new_var(m());
new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(3));
new_exp = m_conv.fu().mk_bv2rm(new_var);
}
else
new_exp = m().mk_var(t->get_idx(), s);