mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

skip entry for origin variable

Browse source
This commit is contained in:
Jakob Rath 2024-03-20 15:37:03 +01:00
parent 23ca9d9fc5
commit fd9c931168
2 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/smt/polysat/project_interval.cpp
View file

@ -179,6 +179,7 @@ namespace polysat {
lbool project_interval::try_project(pvar const w, unsigned const w_off, unsigned const w_sz, rational const& value, unsigned const max_level) {
SASSERT(w != null_var);
SASSERT_EQ(c.size(w), w_sz);
SASSERT(w != m_var);
if (w == m_var)
return l_undef;

5
src/sat/smt/polysat_egraph.cpp
View file

@ -125,7 +125,8 @@ namespace polysat {
// walk the e-graph to retrieve fixed sub-slices along with justifications,
// as well as pvars that correspond to these sub-slices.
void solver::get_fixed_sub_slices(pvar pv, fixed_bits_vector& fixed) {
// does not retrieve a slice corresponding to 'pv' itself.
void solver::get_fixed_sub_slices(pvar const pv, fixed_bits_vector& fixed) {
#define GET_FIXED_SUB_SLICES_DISPLAY 1
auto consume_slice = [&](euf::enode* n, unsigned offset) -> bool {
euf::enode* r = n->get_root();
@ -180,6 +181,8 @@ namespace polysat {
auto const& p = m_var2pdd[s];
if (!p.is_var())
continue;
if (p.var() == pv)
continue;
// unsigned p_level = merge_level(sib, r); // this is ok
#if GET_FIXED_SUB_SLICES_DISPLAY
verbose_stream() << " pvar " << p;