mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
fix #7454
This commit is contained in:
parent
5fd1231ec0
commit
2310514e02
|
@ -150,6 +150,8 @@ void bv_decl_plugin::finalize() {
|
||||||
}
|
}
|
||||||
|
|
||||||
void bv_decl_plugin::mk_bv_sort(unsigned bv_size) {
|
void bv_decl_plugin::mk_bv_sort(unsigned bv_size) {
|
||||||
|
if (bv_size + 1 == 0)
|
||||||
|
throw default_exception("bit-vector of size 2^32-1 are not supported");
|
||||||
force_ptr_array_size(m_bv_sorts, bv_size + 1);
|
force_ptr_array_size(m_bv_sorts, bv_size + 1);
|
||||||
if (!m_bv_sorts[bv_size]) {
|
if (!m_bv_sorts[bv_size]) {
|
||||||
parameter p(bv_size);
|
parameter p(bv_size);
|
||||||
|
|
|
@ -255,9 +255,12 @@ namespace sls {
|
||||||
}
|
}
|
||||||
|
|
||||||
void smt_plugin::sls_phase_to_smt() {
|
void smt_plugin::sls_phase_to_smt() {
|
||||||
|
if (!m_has_new_sls_phase)
|
||||||
|
return;
|
||||||
IF_VERBOSE(2, verbose_stream() << "SLS -> SMT phase\n");
|
IF_VERBOSE(2, verbose_stream() << "SLS -> SMT phase\n");
|
||||||
for (auto v : m_shared_bool_vars)
|
for (auto v : m_shared_bool_vars)
|
||||||
ctx.force_phase(sat::literal(v, !m_sls_phase[v]));
|
ctx.force_phase(sat::literal(v, !m_sls_phase[v]));
|
||||||
|
m_has_new_sls_phase = false;
|
||||||
}
|
}
|
||||||
|
|
||||||
void smt_plugin::sls_activity_to_smt() {
|
void smt_plugin::sls_activity_to_smt() {
|
||||||
|
@ -347,6 +350,7 @@ namespace sls {
|
||||||
expr_ref val(tr(sync_val), m);
|
expr_ref val(tr(sync_val), m);
|
||||||
ctx.set_value(t, val);
|
ctx.set_value(t, val);
|
||||||
}
|
}
|
||||||
|
m_has_new_sls_values = false;
|
||||||
}
|
}
|
||||||
|
|
||||||
void smt_plugin::add_shared_term(expr* t) {
|
void smt_plugin::add_shared_term(expr* t) {
|
||||||
|
|
Loading…
Reference in a new issue