mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

fix the build

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-11-01 12:52:16 -07:00 • committed by Lev Nachmanson
parent 30f5599064
commit e0a08f16d3
1 changed files with 2 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/math/lp/dioph_eq.cpp
View file

@ -418,7 +418,7 @@ namespace lp {
template <typename T> term_o fix_vars(const T& t) const {
term_o ret;
for (auto& p: t) {
for (const auto& p: t) {
if (is_fixed(p.var())) {
ret.c() += p.coeff() * this->lra.get_lower_bound(p.var()).x;
} else {
@ -446,20 +446,6 @@ namespace lp {
subs_front_in_indexed_vector(q);
}
void debug_remove_fresh_vars(term_o& t) {
std::queue<unsigned> q;
for (const auto& p: t) {
if (is_fresh_var(p.j())) {
q.push(p.j());
}
}
while (!q.empty()) {
unsigned j = pop_front(q);
}
}
lia_move tighten_with_S() {
int change = 0;
for (unsigned j = 0; j < lra.column_count(); j++) {
@ -1001,7 +987,7 @@ public:
return j >= lra.column_count();
}
bool can_substitute(unsigned k) {
return k < m_k2s.size() && m_k2s[k] != -1;
return k < m_k2s.size() && m_k2s[k] != UINT_MAX;
}
u_dependency * eq_deps(const lar_term& t) {
NOT_IMPLEMENTED_YET();