mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Check if model_converter is non-null before initializing values in sat_tactic

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-09-23 13:50:32 +01:00
parent 5a6dc18d0d
commit 0604d23c57
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/sat/tactic/sat_tactic.cpp
View file

@ -43,7 +43,8 @@ class sat_tactic : public tactic {
} }
void initialize_values(goal_ref const& g, atom2bool_var& map) { void initialize_values(goal_ref const& g, atom2bool_var& map) {
g->mc()->convert_initialize_value(m_var2value); if (g->mc())
g->mc()->convert_initialize_value(m_var2value);
for (auto & [var, value] : m_var2value) { for (auto & [var, value] : m_var2value) {
if (!m.is_bool(var)) if (!m.is_bool(var))
continue; continue;