mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix #5741
This commit is contained in:
parent
d88f125818
commit
42f206171d
|
@ -605,7 +605,7 @@ private:
|
|||
sub.insert(e, v);
|
||||
expr_ref tmp(m);
|
||||
m_r.set_substitution(&sub);
|
||||
for (unsigned i = 0; i < positions.size(); ++i) {
|
||||
for (unsigned i = 0; !g->inconsistent() && i < positions.size(); ++i) {
|
||||
unsigned idx = positions[i];
|
||||
expr_ref f(m);
|
||||
proof_ref new_pr(m);
|
||||
|
|
|
@ -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 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; }
|
||||
|
||||
|
|
Loading…
Reference in a new issue