mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-16 10:10:02 +00:00
Code Activity

allow calling lp().restore_x() only in case the number of column in lp() remained the same: it might grow

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-03-09 10:51:26 -10:00
parent 4e5695eb53
commit 78fa6d5ee8
3 changed files with 8 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/lar_core_solver.h
View file

@ -81,8 +81,8 @@ public:
void backup_x() { m_backup_x = m_r_x; }
void restore_x() {
SASSERT(m_backup_x.size() == m_r_A.column_count());
m_r_x = m_backup_x;
m_r_x.reserve(m_m());
}
vector<impq> const& r_x() const { return m_r_x; }

4
src/math/lp/nra_solver.cpp
View file

@ -241,16 +241,16 @@ struct solver::imp {
lra.init_model();
for (lp::constraint_index ci : lra.constraints().indices())
if (!check_constraint(ci)) {
VERIFY(!m_coi.constraints().contains(ci));
IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n";
lra.constraints().display(verbose_stream()));
UNREACHABLE();
return l_undef;
}
for (auto const &m : m_nla_core.emons()) {
if (!check_monic(m)) {
VERIFY(!m_coi.mons().contains(m.var()));
IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n";
lra.constraints().display(verbose_stream()));
UNREACHABLE();
return l_undef;
}
}