mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix mixup between sync and sls managed variables

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-28 16:35:50 -08:00
parent fa605454fb
commit d8430810fe
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/sls/sls_smt_plugin.cpp
View file

@ -281,9 +281,9 @@ namespace sls {
expr_ref val_t(m);
if (!ctx.get_smt_value(t, val_t))
continue;
auto t_sls = expr_ref(m_smt2sls_tr(t), m_sls);
auto val_sls = expr_ref(m_smt2sls_tr(val_t.get()), m_sls);
m_sync_var_values.push_back({ t_sls, val_sls });
auto t_sync_ref = expr_ref(t_sync, m_sync);
auto val_sync = expr_ref(m_smt2sync_tr(val_t.get()), m_sync);
m_sync_var_values.push_back({ t_sync_ref, val_sync });
}
m_has_new_smt_values = true;
return;