From d8430810fe64b6be9c21de94ef32df983d562ef5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Jan 2025 16:35:50 -0800 Subject: [PATCH] fix mixup between sync and sls managed variables --- src/ast/sls/sls_smt_plugin.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/sls/sls_smt_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp index fe09b2f010..019a87faf4 100644 --- a/src/ast/sls/sls_smt_plugin.cpp +++ b/src/ast/sls/sls_smt_plugin.cpp @@ -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;