From 974541e24482574f7784218c46296aa8d7e6b4e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Mar 2020 11:44:25 -0700 Subject: [PATCH] fix #3299 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/normalize_bounds_tactic.cpp | 2 +- src/tactic/goal.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index 60d583798..807881503 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -121,7 +121,7 @@ class normalize_bounds_tactic : public tactic { expr_ref new_curr(m); proof_ref new_pr(m); 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); m_rw(curr, new_curr, new_pr); if (produce_proofs) { diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index 757067cb0..286f2864a 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -588,7 +588,7 @@ bool goal::is_well_formed() const { expr * t = form(i); if (!::is_well_sorted(m(), t)) return false; -#if 1 +#if 0 SASSERT(m().get_fact(pr(i)) == form(i)); if (m().get_fact(pr(i)) != form(i)) return false;