From dd211bade9ecb681c2714d6de997f4c91bdf7a2e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Apr 2025 09:40:45 -0700 Subject: [PATCH] filter out terms that are not solved --- src/api/api_qe.cpp | 9 +++++---- src/api/api_solver.cpp | 4 +++- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp index 5424c0330..42407e0ec 100644 --- a/src/api/api_qe.cpp +++ b/src/api/api_qe.cpp @@ -95,10 +95,11 @@ extern "C" obj_map &map_z3 = to_ast_map_ref(map); - for (auto& kv : emap) { - m.inc_ref(kv.m_key); - m.inc_ref(kv.m_value); - map_z3.insert(kv.m_key, kv.m_value); + for (auto& [k,v] : emap) { + SASSERT(v); + m.inc_ref(k); + m.inc_ref(v); + map_z3.insert(k, v); } return of_expr (result); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index a7bafc0bc..13a6c1930 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -995,9 +995,11 @@ extern "C" { _terms.reset(); _guards.reset(); for (solver::solution const& s : solutions) { + if (!s.term) + continue; _vars.push_back(s.var); _terms.push_back(s.term); - _guards.push_back(s.guard); + _guards.push_back(s.guard ? s.guard : m.mk_true()); } Z3_CATCH; }