mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

fix fix

Browse source
This commit is contained in:
Jakob Rath 2023-11-06 15:10:13 +01:00
parent f09d37f93f
commit 50eb43500e
1 changed files with 4 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/polysat/slicing.cpp
View file

@ -916,17 +916,16 @@ namespace polysat {
// exactly one node has a value // exactly one node has a value
rational const val = get_value(v); rational const val = get_value(v);
for (enode* n : euf::enode_class(other)) { for (enode* n : euf::enode_class(other)) {
pvar const var = slice2var(n);
if (var != null_var && m_solver.is_assigned(var))
continue; // TODO: could try to detect possible conflicts by checking value
enode* const vn = get_value_node(n); enode* const vn = get_value_node(n);
if (!vn) if (!vn)
set_value_node(n, v); set_value_node(n, v);
pvar const var = slice2var(n);
if (var == null_var) if (var == null_var)
continue; continue;
LOG("on_merge: v" << v << " := " << val); if (m_solver.is_assigned(var))
continue;
LOG("on_merge: v" << var << " := " << val);
m_solver.assign_propagate_by_slicing(var, val); m_solver.assign_propagate_by_slicing(var, val);
} }
} }