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

Update theory_lra.cpp

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-09-23 16:26:31 -07:00 committed by GitHub
parent acad9fa62c
commit a3e2e68d93
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_lra.cpp
View file

@ -1480,7 +1480,6 @@ public:
m_model_eqs.reset(); m_model_eqs.reset();
svector<lpvar> vars; svector<lpvar> vars;
theory_var sz = static_cast<theory_var>(th.get_num_vars()); theory_var sz = static_cast<theory_var>(th.get_num_vars());
verbose_stream() << "check " << sz << "\n";
for (theory_var v = 0; v < sz; ++v) { for (theory_var v = 0; v < sz; ++v) {
enode * n1 = get_enode(v); enode * n1 = get_enode(v);
if (!th.is_relevant_and_shared(n1)) { if (!th.is_relevant_and_shared(n1)) {