mirror of
https://github.com/Z3Prover/z3
synced 2025-07-23 12:48:53 +00:00
parent
c613ab0ba0
commit
974541e244
2 changed files with 2 additions and 2 deletions
|
@ -121,7 +121,7 @@ class normalize_bounds_tactic : public tactic {
|
||||||
expr_ref new_curr(m);
|
expr_ref new_curr(m);
|
||||||
proof_ref new_pr(m);
|
proof_ref new_pr(m);
|
||||||
unsigned size = in->size();
|
unsigned size = in->size();
|
||||||
for (unsigned idx = 0; idx < size; idx++) {
|
for (unsigned idx = 0; !in->inconsistent() && idx < size; idx++) {
|
||||||
expr * curr = in->form(idx);
|
expr * curr = in->form(idx);
|
||||||
m_rw(curr, new_curr, new_pr);
|
m_rw(curr, new_curr, new_pr);
|
||||||
if (produce_proofs) {
|
if (produce_proofs) {
|
||||||
|
|
|
@ -588,7 +588,7 @@ bool goal::is_well_formed() const {
|
||||||
expr * t = form(i);
|
expr * t = form(i);
|
||||||
if (!::is_well_sorted(m(), t))
|
if (!::is_well_sorted(m(), t))
|
||||||
return false;
|
return false;
|
||||||
#if 1
|
#if 0
|
||||||
SASSERT(m().get_fact(pr(i)) == form(i));
|
SASSERT(m().get_fact(pr(i)) == form(i));
|
||||||
if (m().get_fact(pr(i)) != form(i))
|
if (m().get_fact(pr(i)) != form(i))
|
||||||
return false;
|
return false;
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue