mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

fix get_name for variables

Browse source
This commit is contained in:
Jakob Rath 2023-07-19 12:40:18 +02:00
parent 85d80a0ae1
commit b67caf5fc3
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polysat/naming.cpp
View file

@ -43,6 +43,8 @@ namespace polysat {
} }
pvar name_manager::get_name(pdd const& t) const { pvar name_manager::get_name(pdd const& t) const {
if (t.is_var())
return t.var();
name_key key{t}; name_key key{t};
auto it = m_names.find_iterator(key); auto it = m_names.find_iterator(key);
if (it == m_names.end()) if (it == m_names.end())
@ -53,6 +55,7 @@ namespace polysat {
pvar name_manager::mk_name(pdd const& t) { pvar name_manager::mk_name(pdd const& t) {
if (t.is_var()) if (t.is_var())
return t.var(); return t.var();
SASSERT(!t.is_val()); // we probably don't want names for constants
pvar v = get_name(t); pvar v = get_name(t);
if (v != null_var) if (v != null_var)
return v; return v;