diff options
| author | N. Engelhardt <nak@symbioticeda.com> | 2020-05-20 08:55:36 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-05-20 08:55:36 +0200 |
| commit | 7c4e580f8f9b5f441f3af5454e68cba38eb52e91 (patch) | |
| tree | 0f799b94ab1201aef4099568936526b76da34d59 | |
| parent | aee439360bba642dcbffe5b803aa9a994b11d183 (diff) | |
| parent | 1053032a81ea54847bfef944d3c5481de8a2046e (diff) | |
| download | yosys-7c4e580f8f9b5f441f3af5454e68cba38eb52e91.tar.gz yosys-7c4e580f8f9b5f441f3af5454e68cba38eb52e91.tar.bz2 yosys-7c4e580f8f9b5f441f3af5454e68cba38eb52e91.zip | |
Merge pull request #2054 from boqwxp/fix-smtbmc
smtbmc: Fix return status handling.
| -rw-r--r-- | backends/smt2/smtbmc.py | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index d3015b066..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) @@ -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, '%') |