mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-06 22:36:03 +00:00
Code Activity

#5732

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-22 18:04:53 -08:00
parent 8fd89c5e15
commit 84ddd06c8f
2 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/core/pb_preprocess_tactic.cpp
View file

@ -196,6 +196,8 @@ public:
// now check for subsumption.
for (unsigned i = 0; i < m_ge.size(); ++i) {
if (g->inconsistent())
break;
expr_ref_vector args1(m), args2(m);
vector<rational> coeffs1, coeffs2;
@ -209,7 +211,7 @@ public:
if (!m_vars.contains(to_app(arg))) continue;
rec const& r = m_vars.find(to_app(arg));
unsigned_vector const& pos = neg?r.neg:r.pos;
for (unsigned j = 0; j < pos.size(); ++j) {
for (unsigned j = 0; !g->inconsistent() && j < pos.size(); ++j) {
unsigned k = pos[j];
if (k == m_ge[i]) continue;
if (!to_ge(g->form(k), args2, coeffs2, k2)) continue;

2
src/tactic/goal.h
View file

@ -119,7 +119,7 @@ public:
unsigned num_exprs() const;
expr * form(unsigned i) const { return m().get(m_forms, i); }
expr * form(unsigned i) const { return m_inconsistent ? m().mk_false() : m().get(m_forms, i); }
proof * pr(unsigned i) const { return m().size(m_proofs) > i ? static_cast<proof*>(m().get(m_proofs, i)) : nullptr; }
expr_dependency * dep(unsigned i) const { return unsat_core_enabled() ? m().get(m_dependencies, i) : nullptr; }