mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

#5215

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-27 15:40:17 -07:00
parent e5892e5e97
commit 4da4591fe7
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/sat/smt/euf_model.cpp
View file

@ -144,6 +144,16 @@ namespace euf {
m_values.set(id, m.mk_false()); m_values.set(id, m.mk_false());
continue; continue;
} }
switch (n->value()) {
case l_true:
m_values.set(id, m.mk_true());
continue;
case l_false:
m_values.set(id, m.mk_false());
continue;
default:
break;
}
if (is_app(e) && to_app(e)->get_family_id() == m.get_basic_family_id()) if (is_app(e) && to_app(e)->get_family_id() == m.get_basic_family_id())
continue; continue;
sat::bool_var v = get_enode(e)->bool_var(); sat::bool_var v = get_enode(e)->bool_var();