riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #2054 from boqwxp/fix-smtbmc 

smtbmc: Fix return status handling.
This commit is contained in:
N. Engelhardt 2020-05-20 08:55:36 +02:00 committed by GitHub
parent aee439360b 1053032a81
commit 7c4e580f8f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
backends/smt2/smtbmc.py
View File

@ -1511,7 +1511,7 @@ else: # not tempind, covermode
smt_assert_consequent(get_constr_expr(constr_assumes, i)) smt_assert_consequent(get_constr_expr(constr_assumes, i))
print_msg("Re-solving with appended steps..") print_msg("Re-solving with appended steps..")
if smt_check_sat() == "unsat": 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" retstatus = "FAILED"
break break
print_anyconsts(step) print_anyconsts(step)
@ -1548,7 +1548,7 @@ else: # not tempind, covermode
break break
smt_pop() smt_pop()
if not retstatus: if retstatus == "FAILED" or retstatus == "PREUNSAT":
break break
else: # gentrace else: # gentrace
@ -1568,7 +1568,7 @@ else: # not tempind, covermode
step += step_size step += step_size
if gentrace and retstatus: if gentrace and retstatus == "PASSED":
print_anyconsts(0) print_anyconsts(0)
write_trace(0, num_steps, '%') write_trace(0, num_steps, '%')