From 7d88d045149ae10da2609455be1a608ec82f1564 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Apr 2015 00:55:30 +0200 Subject: [PATCH] fix crash reported by Jojanovich, github issue 45' Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/fix_dl_var_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index 693066ee1..6d9f98f39 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -282,7 +282,7 @@ class fix_dl_var_tactic : public tactic { expr_ref new_curr(m); proof_ref new_pr(m); unsigned size = g->size(); - for (unsigned idx = 0; idx < size; idx++) { + for (unsigned idx = 0; !g->inconsistent() && idx < size; idx++) { expr * curr = g->form(idx); m_rw(curr, new_curr, new_pr); if (produce_proofs) {