From 299ab76a093f0cde95fdc0214b371140d7f339b9 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Thu, 14 May 2020 17:07:59 +0000 Subject: smtbmc: Fix return status handling. --- backends/smt2/smtbmc.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index d3015b066..f1f55be1c 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1548,7 +1548,7 @@ else: # not tempind, covermode break smt_pop() - if not retstatus: + if retstatus == "FAILED" or retstatus == "PREUNSAT": break else: # gentrace @@ -1568,7 +1568,7 @@ else: # not tempind, covermode step += step_size - if gentrace and retstatus: + if gentrace and retstatus == "PASSED": print_anyconsts(0) write_trace(0, num_steps, '%') -- cgit v1.2.3 From 1053032a81ea54847bfef944d3c5481de8a2046e Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Tue, 19 May 2020 16:13:44 +0000 Subject: smtbmc: Fix typo in error message. Co-Authored-By: N. Engelhardt --- backends/smt2/smtbmc.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index f1f55be1c..cc3ebb129 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1511,7 +1511,7 @@ else: # not tempind, covermode 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()) + print("%s Cannot append steps without violating assumptions!" % smt.timestamp()) retstatus = "FAILED" break print_anyconsts(step) -- cgit v1.2.3