From bacca5753775bfabed955a9772a5d86d85007c58 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 13 Mar 2019 19:27:17 +0100
Subject: [PATCH] Fix smtbmc.py handling of zero appended steps
Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
backends/smt2/smtbmc.py | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 94a5e2da0..445a42e0d 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -1484,11 +1484,11 @@ else: # not tempind, covermode
smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
smt_assert_consequent(get_constr_expr(constr_assumes, i))
- print_msg("Re-solving with appended steps..")
- if smt_check_sat() == "unsat":
- print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
- retstatus = False
- break
+ print_msg("Re-solving with appended steps..")
+ if smt_check_sat() == "unsat":
+ print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
+ retstatus = False
+ break
print_anyconsts(step)
for i in range(step, last_check_step+1):
print_failed_asserts(i)