mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-07 14:45:18 +00:00
Code Activity

Add "Unexpected response" handling to smtbmc engine

Browse source 
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
This commit is contained in:
Claire Wolf 2020-07-20 19:42:10 +02:00
parent 42d5255231
commit 0d98201dc7
2 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
docs/examples/puzzles/primegen.sby
View file

@ -6,7 +6,7 @@ primes_pass
[options] [options]
mode cover mode cover
depth 1 depth 1
primes_fail: expect fail primes_fail: expect fail,error
[engines] [engines]
smtbmc --dumpsmt2 --progress --stbv z3 smtbmc --dumpsmt2 --progress --stbv z3

6
sbysrc/sby_engine_smtbmc.py
View file

@ -37,7 +37,6 @@ def run(mode, job, engine_idx, engine):
"nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="]) "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="])
for o, a in opts: for o, a in opts:
print(o, a)
if o == "--nomem": if o == "--nomem":
nomem_opt = True nomem_opt = True
elif o == "--syn": elif o == "--syn":
@ -169,6 +168,11 @@ def run(mode, job, engine_idx, engine):
task_status = "ERROR" task_status = "ERROR"
return line return line
match = re.match(r"^## [0-9: ]+ Unexpected response from solver:", line)
if match:
task_status = "ERROR"
return line
return line return line
def exit_callback(retcode): def exit_callback(retcode):