From 4eb91d5b883f05f6c2c4f655315ce5b16a724a44 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 22 Nov 2018 17:08:28 +0100 Subject: [PATCH] Add "smtbmc ... -- ..." feature (for "raw" smtbmc options) Signed-off-by: Clifford Wolf --- docs/source/reference.rst | 2 ++ sbysrc/sby_engine_smtbmc.py | 9 ++++++++- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 5143fd8..26232a9 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -241,6 +241,8 @@ The following solvers are currently supported by ``yosys-smtbmc``: * mathsat * cvc4 +Any additional options after ``--`` are passed to ``yosys-smtbmc`` as-is. + ``aiger`` engine ~~~~~~~~~~~~~~~~ diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index ec83c27..38bde62 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -67,10 +67,17 @@ def run(mode, job, engine_idx, engine): else: job.error("Invalid smtbmc options %s." % o) + xtra_opts = False for i, a in enumerate(args): if i == 0 and a == "z3" and unroll_opt is None: unroll_opt = False - smtbmc_opts += ["-s" if i == 0 else "-S", a] + if a == "--": + xtra_opts = True + continue + if xtra_opts: + smtbmc_opts.append(a) + else: + smtbmc_opts += ["-s" if i == 0 else "-S", a] if presat_opt: smtbmc_opts += ["--presat"] -- 2.30.2