From 0d98201dc7ae78e41c410354448dcee7a811fd4f Mon Sep 17 00:00:00 2001 From: Claire Wolf Date: Mon, 20 Jul 2020 19:42:10 +0200 Subject: [PATCH] Add "Unexpected response" handling to smtbmc engine Signed-off-by: Claire Wolf --- docs/examples/puzzles/primegen.sby | 2 +- sbysrc/sby_engine_smtbmc.py | 6 +++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/docs/examples/puzzles/primegen.sby b/docs/examples/puzzles/primegen.sby index 20e5072..6d88b88 100644 --- a/docs/examples/puzzles/primegen.sby +++ b/docs/examples/puzzles/primegen.sby @@ -6,7 +6,7 @@ primes_pass [options] mode cover depth 1 -primes_fail: expect fail +primes_fail: expect fail,error [engines] smtbmc --dumpsmt2 --progress --stbv z3 diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 65933d0..6d2ffc4 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -37,7 +37,6 @@ def run(mode, job, engine_idx, engine): "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="]) for o, a in opts: - print(o, a) if o == "--nomem": nomem_opt = True elif o == "--syn": @@ -169,6 +168,11 @@ def run(mode, job, engine_idx, engine): task_status = "ERROR" return line + match = re.match(r"^## [0-9: ]+ Unexpected response from solver:", line) + if match: + task_status = "ERROR" + return line + return line def exit_callback(retcode): -- 2.30.2